1 agosto 2023 – Calculemus

Si R es un anillo y a, b, c ∈ R tales que a+b=a+c, entonces b=c

PorJosé A. Alonso 1 agosto 202327 julio 2023

Demostrar con Lean4 que si R es un anillo y a, b, c ∈ R tales que

   a + b = a + c

1	a + b = a + c

entonces

   b = c

b = c

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Algebra.Ring.Defs
import Mathlib.Tactic

variable {R : Type _} [Ring R]
variable {a b c : R}

example
  (h : a + b = a + c)
  : b = c :=
sorry

import Mathlib.Algebra.Ring.Defs

import Mathlib.Tactic

variable {R : Type _} [Ring R]

variable {a b c : R}

example

(h : a + b = a + c)

: b = c :=

sorry