Si G es un grupo y a ∈ G, entonces a * 1 = a
Demostrar que si G es un grupo y a ∈ G, entonces
|
1 |
a * 1 = a |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import algebra.group variables {G : Type*} [group G] variables a : G example : a * 1 = 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 46 |
import algebra.group variables {G : Type*} [group G] variables a : G -- 1ª demostración -- =============== example : a * 1 = a := calc a * 1 = a * (a⁻¹ * a) : congr_arg (λ x, a * x) (mul_left_inv a).symm ... = (a * a⁻¹) * a : (mul_assoc a a⁻¹ a).symm ... = 1 * a : congr_arg (λ x, x* a) (mul_right_inv a) ... = a : one_mul a -- 2ª demostración -- =============== example : a * 1 = a := calc a * 1 = a * (a⁻¹ * a) : by rw mul_left_inv ... = (a * a⁻¹) * a : by rw mul_assoc ... = 1 * a : by rw mul_right_inv ... = a : by rw one_mul -- 3ª demostración -- =============== example : a * 1 = a := calc a * 1 = a * (a⁻¹ * a) : by simp ... = (a * a⁻¹) * a : by simp ... = 1 * a : by simp ... = a : by simp -- 3ª demostración -- =============== example : a * 1 = a := by simp -- 4ª demostración -- =============== example : a * 1 = a := -- by library_search mul_one 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. 14.
