Si R es un anillo y a ∈ R, entonces 2 * a = a + a
Demostrar que si R es un anillo y a ∈ R, entonces
|
1 |
2 * a = a + 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 : R example : 2 * a = a + 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 44 45 |
import algebra.ring variables {R : Type*} [ring R] variables a : R -- 1ª demostración -- =============== example : 2 * a = a + a := calc 2 * a = (1 + 1) * a : congr_fun (congr_arg has_mul.mul one_add_one_eq_two.symm) a ... = 1 * a + 1 * a : add_mul 1 1 a ... = a + 1 * a : congr_arg (λ x, x + 1 * a) (one_mul a) ... = a + a : congr_arg (λ x, a + x) (one_mul a) -- 2ª demostración -- =============== example : 2 * a = a + a := calc 2 * a = (1 + 1) * a : by rw one_add_one_eq_two ... = 1 * a + 1 * a : by rw add_mul ... = a + a : by rw one_mul -- 3ª demostración -- =============== example : 2 * a = a + a := by rw [one_add_one_eq_two.symm, add_mul, one_mul] -- 4ª demostración -- =============== example : 2 * a = a + a := calc 2 * a = (1 + 1) * a : rfl ... = 1 * a + 1 * a : by simp [add_mul] ... = a + a : by simp -- 5ª demostración -- =============== example : 2 * a = a + a := -- by library_search two_mul a |
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.
