Si R es un anillo y a, b ∈ R, entonces (a + b) + -b = a
Demostrar que si R es un anillo, entonces
|
1 |
∀ a b : R, (a + b) + -b = a |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import algebra.ring variables {R : Type*} [ring R] variables a b : R example : (a + b) + -b = a := sorry |
Soluciones con Lean
|
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 |
import algebra.ring variables {R : Type*} [ring R] variables a b : R -- 1ª demostración -- =============== example : (a + b) + -b = a := calc (a + b) + -b = a + (b + -b) : by rw add_assoc ... = a + 0 : by rw add_right_neg ... = a : by rw add_zero -- 2ª demostración -- =============== example : (a + b) + -b = a := begin rw add_assoc, rw add_right_neg, rw add_zero, end -- 3ª demostración -- =============== example : (a + b) + -b = a := by rw [add_assoc, add_right_neg, add_zero] -- 4ª demostración -- =============== example : (a + b) + -b = a := -- by library_search add_neg_eq_of_eq_add rfl -- 5ª demostración -- =============== example : (a + b) + -b = a := -- by hint by finish |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 11.
