Si R es un anillo y a, b ∈ R tales que a+b=0, entonces -a=b
Demostrar con Lean4 que si R es un anillo y a, b ∈ R tales que
1 |
a + b = 0 |
entonces
1 |
-a = b |
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable {a b : R} example (h : a + b = 0) : -a = b := sorry |
Demostraciones en lenguaje natural (LN)
1ª demostración en LN
Por la siguiente cadena de igualdades
\begin{align}
-a &= -a + 0 &&\text{[por suma cero]} \\
&= -a + (a + b) &&\text{[por hipótesis]} \\
&= b &&\text{[por cancelativa]}
\end{align}
2ª demostración en LN
Sumando \(-a\) a ambos lados de la hipótesis, se tiene
\[-a + (a + b) = -a + 0\]
El término de la izquierda se reduce a \(b\) (por la cancelativa) y el de la derecha a \(-a\) (por la suma con cero). Por tanto, se tiene
\[b = -a\]
Por la simetría de la igualdad, se tiene
\[-a = b\]
Demostraciones con Lean4
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable {a b : R} -- 1ª demostración (basada en la 1º en LN) example (h : a + b = 0) : -a = b := calc -a = -a + 0 := by rw [add_zero] _ = -a + (a + b) := by rw [h] _ = b := by rw [neg_add_cancel_left] -- 2ª demostración (basada en la 1º en LN) example (h : a + b = 0) : -a = b := calc -a = -a + 0 := by simp _ = -a + (a + b) := by rw [h] _ = b := by simp -- 3ª demostración (basada en la 2º en LN) example (h : a + b = 0) : -a = b := by have h1 : -a + (a + b) = -a + 0 := congrArg (HAdd.hAdd (-a)) h have h2 : -a + (a + b) = b := neg_add_cancel_left a b have h3 : -a + 0 = -a := add_zero (-a) rw [h2, h3] at h1 exact h1.symm -- 4ª demostración (con la librería mathlib) example (h : a + b = 0) : -a = b := neg_eq_iff_add_eq_zero.mpr h |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 11.