2 agosto 2023 – Calculemus

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

PorJosé A. Alonso 2 agosto 202327 julio 2023

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

   a + b = c + b

1	a + b = c + b

entonces

   a = c

a = 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 = c + b)
  : a = c :=
sorry

import Mathlib.Algebra.Ring.Defs

import Mathlib.Tactic

variable {R : Type _} [Ring R]

variable {a b c : R}

example

(h : a + b = c + b)

: a = c :=

sorry