Si R es un anillo y a ∈ R, entonces a * 0 = 0
Demostrar que Si R es un anillo y a ∈ R, entonces
1 |
a * 0 = 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 : a * 0 = 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 60 61 62 63 64 65 66 |
import algebra.ring variables {R : Type*} [ring R] variable a : R -- 1ª demostración -- =============== example : a * 0 = 0 := begin have h : a * 0 + a * 0 = a * 0 + 0, calc a * 0 + a * 0 = a * (0 + 0) : (mul_add a 0 0).symm ... = a * 0 : congr_arg (λ x, a * x) (add_zero 0) ... = a * 0 + 0 : (add_zero (a * 0)).symm, rw add_left_cancel h end -- 2ª demostración -- =============== example : a * 0 = 0 := begin have h : a * 0 + a * 0 = a * 0 + 0, calc a * 0 + a * 0 = a * (0 + 0) : by rw ←mul_add ... = a * 0 : by rw add_zero ... = a * 0 + 0 : by rw add_zero, rw add_left_cancel h end -- 3ª demostración -- =============== example : a * 0 = 0 := begin have h : a * 0 + a * 0 = a * 0 + 0, { rw [←mul_add, add_zero, add_zero] }, rw add_left_cancel h end -- 4ª demostración -- =============== example : a * 0 = 0 := begin have h : a * 0 + a * 0 = a * 0 + 0, calc a * 0 + a * 0 = a * (0 + 0) : by simp ... = a * 0 : by simp ... = a * 0 + 0 : by simp, simp, end -- 5ª demostración -- =============== example : a * 0 = 0 := by simp -- 6ª demostración -- =============== example : a * 0 = 0 := -- by library_search mul_zero 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. 12.