Si R es un anillo y a,b∈R tales que a+b=0, entonces a=-b
Demostrar 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 Lean:
|
1 2 3 4 5 6 7 8 9 |
import algebra.ring variables {R : Type*} [ring R] variables {a b : R} example (h : a + b = 0) : a = -b := 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 44 45 46 47 48 49 50 51 52 |
import algebra.ring variables {R : Type*} [ring R] variables {a b : R} -- 1ª demostración -- =============== example (h : a + b = 0) : a = -b := calc a = a + 0 : (add_zero a).symm ... = a + (b + -b) : congr_arg (λ x, a + x) (add_neg_self b).symm ... = (a + b) + -b : (add_assoc a b (-b)).symm ... = 0 + -b : congr_arg (λ x, x + -b) h ... = -b : zero_add (-b) -- 2ª demostración -- =============== example (h : a + b = 0) : a = -b := calc a = a + 0 : by rw add_zero ... = a + (b + -b) : by {congr ; rw add_neg_self} ... = (a + b) + -b : by rw add_assoc ... = 0 + -b : by {congr; rw h} ... = -b : by rw zero_add -- 3ª demostración -- =============== example (h : a + b = 0) : a = -b := calc a = a + 0 : by simp ... = a + (b + -b) : by simp ... = (a + b) + -b : by simp ... = 0 + -b : by simp [h] ... = -b : by simp -- 4ª demostración -- =============== example (h : a + b = 0) : a = -b := -- by library_search add_eq_zero_iff_eq_neg.mp h |
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. 12.
