Si R es un anillo y a, b, c ∈ R tales que a+b=c+b, entonces a=c
Demostrar con Lean4 que si R es un anillo y a, b, c ∈ R tales que
|
1 |
a + b = c + b |
entonces
|
1 |
a = c |
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 c : R} example (h : a + b = c + b) : a = c := 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 con cero]} \\
&= a + (b + -b) &&\text{[por suma con opuesto]} \\
&= (a + b) + -b &&\text{[por asociativa]} \\
&= (c + b) + -b &&\text{[por hipótesis]} \\
&= c + (b + -b) &&\text{[por asociativa]} \\
&= c + 0 &&\text{[por suma con opuesto]} \\
&= c &&\text{[por suma con cero]}
\end{align}
2ª demostración en LN
Por la siguiente cadena de igualdades
\begin{align}
a &= (a + b) + -b \\
&= (c + b) + -b &&\text{[por hipótesis]} \\
&= c
\end{align}
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 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable {a b c : R} -- 1ª demostración con Lean4 -- ========================= example (h : a + b = c + b) : a = c := calc a = a + 0 := by rw [add_zero] _ = a + (b + -b) := by rw [add_right_neg] _ = (a + b) + -b := by rw [add_assoc] _ = (c + b) + -b := by rw [h] _ = c + (b + -b) := by rw [← add_assoc] _ = c + 0 := by rw [← add_right_neg] _ = c := by rw [add_zero] -- 2ª demostración con Lean4 -- ========================= example (h : a + b = c + b) : a = c := calc a = (a + b) + -b := (add_neg_cancel_right a b).symm _ = (c + b) + -b := by rw [h] _ = c := add_neg_cancel_right c b -- 3ª demostración con Lean4 -- ========================= example (h : a + b = c + b) : a = c := by rw [← add_neg_cancel_right a b] rw [h] rw [add_neg_cancel_right] -- 4ª demostración con Lean4 -- ========================= example (h : a + b = c + b) : a = c := by rw [← add_neg_cancel_right a b, h, add_neg_cancel_right] -- 5ª demostración con Lean4 -- ========================= example (h : a + b = c + b) : a = c := add_right_cancel 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.
