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