Si R es un anillo y a ∈ R, entonces 0 * a = 0
Demostrar que si R es un anillo y a ∈ R, entonces
1 |
0 * a = 0. |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 |
import algebra.ring variables {R : Type*} [ring R] variable (a : R) example : 0 * a = 0 := 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 59 |
import algebra.ring variables {R : Type*} [ring R] variable (a : R) -- 1ª demostración -- =============== example : 0 * a = 0 := begin have h : 0 * a + 0 * a = 0 * a + 0, calc 0 * a + 0 * a = (0 + 0) * a : (add_mul 0 0 a).symm ... = 0 * a : congr_arg (λ x, x * a) (add_zero 0) ... = 0 * a + 0 : self_eq_add_right.mpr rfl, rw add_left_cancel h end -- 2ª demostración -- =============== example : 0 * a = 0 := begin have h : 0 * a + 0 * a = 0 * a + 0, calc 0 * a + 0 * a = (0 + 0) * a : by rw add_mul ... = 0 * a : by rw add_zero ... = 0 * a + 0 : by rw add_zero, rw add_left_cancel h end -- 3ª demostración -- =============== example : 0 * a = 0 := begin have h : 0 * a + 0 * a = 0 * a + 0, { rw [←add_mul, add_zero, add_zero] }, rw add_left_cancel h end -- 4ª demostración -- =============== example : 0 * a = 0 := begin have h : 0 * a + 0 * a = 0 * a + 0, calc 0 * a + 0 * a = (0 + 0) * a : by simp ... = 0 * a : by simp ... = 0 * a + 0 : by simp, simp, end -- 5ª demostración -- =============== example : 0 * a = 0 := by simp |
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.