Si R es un anillo y a, b, c ∈ R tales que a+b=a+c, entonces b=c
Demostrar con Lean4 que si R es un anillo y a, b, c ∈ R tales que
|
1 |
a + b = a + c |
entonces
|
1 |
b = 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 = a + c) : b = c := sorry |
Demostración en lenguaje natural (LN)
1ª demostración en LN
Por la siguiente cadena de igualdades
\begin{align}
b &= 0 + b &&\text{[por suma con cero]} \\
&= (-a + a) + b &&\text{[por suma con opuesto]} \\
&= -a + (a + b) &&\text{[por asociativa]} \\
&= -a + (a + c) &&\text{[por hipótesis]} \\
&= (-a + a) + c &&\text{[por asociativa]} \\
&= 0 + c &&\text{[por suma con opuesto]} \\
&= c &&\text{[por suma con cero]}
\end{align}
2ª demostración en LN
Por la siguiente cadena de implicaciones
\begin{align}
a + b = a + c
&\Longrightarrow -a + (a + b) = -a + (a + c) &&\text{[sumando -a]} \\
&\Longrightarrow (-a + a) + b = (-a + a) + c &&\text{[por la asociativa]} \\
&\Longrightarrow 0 + b = 0 + b &&\text{[suma con opuesto]} \\
&\Longrightarrow b = c &&\text{[suma con cero]}
\end{align}
3ª demostración en LN
Por la siguiente cadena de igualdades
\begin{align}
b &= -a + (a + b) \\
&= -a + (a + c) &&\text{[por la 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 60 61 62 63 64 65 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable {a b c : R} -- 1ª demostración example (h : a + b = a + c) : b = c := calc b = 0 + b := by rw [zero_add] _ = (-a + a) + b := by rw [add_left_neg] _ = -a + (a + b) := by rw [add_assoc] _ = -a + (a + c) := by rw [h] _ = (-a + a) + c := by rw [←add_assoc] _ = 0 + c := by rw [add_left_neg] _ = c := by rw [zero_add] -- 2ª demostración example (h : a + b = a + c) : b = c := by have h1 : -a + (a + b) = -a + (a + c) := congrArg (HAdd.hAdd (-a)) h clear h rw [← add_assoc] at h1 rw [add_left_neg] at h1 rw [zero_add] at h1 rw [← add_assoc] at h1 rw [add_left_neg] at h1 rw [zero_add] at h1 exact h1 -- 3ª demostración example (h : a + b = a + c) : b = c := calc b = -a + (a + b) := by rw [neg_add_cancel_left a b] _ = -a + (a + c) := by rw [h] _ = c := by rw [neg_add_cancel_left] -- 4ª demostración example (h : a + b = a + c) : b = c := by rw [← neg_add_cancel_left a b] rw [h] rw [neg_add_cancel_left] -- 5ª demostración example (h : a + b = a + c) : b = c := by rw [← neg_add_cancel_left a b, h, neg_add_cancel_left] -- 6ª demostración example (h : a + b = a + c) : b = c := add_left_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.
