Si R es un anillo y a, b ∈ R, entonces a – b = a + -b
Demostrar que si R es un anillo y a, b ∈ R, entonces
|
1 |
a - b = a + -b |
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 = 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 53 54 55 56 57 58 |
import algebra.ring variables {R : Type*} [ring R] variables {a b : R} -- 1ª demostración -- =============== example : a - b = a + -b := begin apply sub_eq_iff_eq_add.mpr, calc a = a + 0 : (add_zero a).symm ... = a + (-b + b) : congr_arg (λ x, a + x) (neg_add_self b).symm ... = a + -b + b : (add_assoc a (-b) b).symm end -- 2ª demostración -- =============== example : a - b = a + -b := begin apply sub_eq_iff_eq_add.mpr, calc a = a + 0 : by rw add_zero ... = a + (-b + b) : by {congr; rw neg_add_self} ... = a + -b + b : by rw add_assoc end -- 3ª demostración -- =============== example : a - b = a + -b := begin rw sub_eq_iff_eq_add, rw add_assoc, rw neg_add_self, rw add_zero, end -- 4ª demostración -- =============== example : a - b = a + -b := by rw [sub_eq_iff_eq_add, add_assoc, neg_add_self, add_zero] -- 5ª demostración -- =============== example : a - b = a + -b := by simp [sub_eq_iff_eq_add] -- 6ª demostración -- =============== example : a - b = a + -b := -- by library_search sub_eq_add_neg a b |
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. 13.
