Si R es un anillo y a ∈ R, entonces -(-a) = a
Demostrar con Lean4 que si R es un anillo y a ∈ R, entonces
|
1 |
-(-a) = a |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable {a : R} example : -(-a) = a := sorry |
Demostración en lenguaje natural
Es consecuencia de las siguiente propiedades demostradas en ejercicios anteriores:
\begin{align}
&\forall a \ b \in R, a + b = 0 \to -a = b \\
&\forall a \in R, -a + a = 0
\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 |
import Mathlib.Algebra.Ring.Defs import Mathlib.Tactic variable {R : Type _} [Ring R] variable {a : R} -- 1ª demostración example : -(-a) = a := by have h1 : -a + a = 0 := add_left_neg a show -(-a) = a exact neg_eq_of_add_eq_zero_right h1 -- 2ª demostración example : -(-a) = a := by apply neg_eq_of_add_eq_zero_right rw [add_left_neg] -- 3ª demostración example : -(-a) = a := neg_neg a -- 4ª demostración example : -(-a) = a := by simp |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 11.
