Si G un grupo y a ∈ G, entonces (a⁻¹)⁻¹ = a
Demostrar con Lean4 que si \(G\) un grupo y \(a ∈ G\), entonces
\[(a⁻¹)⁻¹ = a\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] variable {a : G} example : (a⁻¹)⁻¹ = a := sorry |
1. Demostración en lenguaje natural
Por la siguiente cadena de igualdades
\begin{align}
(a⁻¹)⁻¹ &= (a⁻¹)⁻¹·1 &&\text{[porque \(1\) es neutro]} \\
&= (a⁻¹)⁻¹·(a⁻¹·a) &&\text{[porque \(a⁻¹\) es el inverso de \(a\)]} \\
&= ((a⁻¹)⁻¹·a⁻¹)·a &&\text{[por la asociativa]} \\
&= 1·a &&\text{[porque \((a⁻¹)⁻¹\) es el inverso de \(a⁻¹\)]} \\
&= a &&\text{[porque \(1\) es neutro]}
\end{align}
2. Demostraciones con Lean4
|
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 67 68 69 70 71 72 73 74 75 76 |
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] variable {a : G} -- 1ª demostración -- =============== example : (a⁻¹)⁻¹ = a := calc (a⁻¹)⁻¹ = (a⁻¹)⁻¹ * 1 := (mul_one (a⁻¹)⁻¹).symm _ = (a⁻¹)⁻¹ * (a⁻¹ * a) := congrArg ((a⁻¹)⁻¹ * .) (inv_mul_self a).symm _ = ((a⁻¹)⁻¹ * a⁻¹) * a := (mul_assoc _ _ _).symm _ = 1 * a := congrArg (. * a) (inv_mul_self a⁻¹) _ = a := one_mul a -- 2ª demostración -- =============== example : (a⁻¹)⁻¹ = a := calc (a⁻¹)⁻¹ = (a⁻¹)⁻¹ * 1 := by simp only [mul_one] _ = (a⁻¹)⁻¹ * (a⁻¹ * a) := by simp only [inv_mul_self] _ = ((a⁻¹)⁻¹ * a⁻¹) * a := by simp only [mul_assoc] _ = 1 * a := by simp only [inv_mul_self] _ = a := by simp only [one_mul] -- 3ª demostración -- =============== example : (a⁻¹)⁻¹ = a := calc (a⁻¹)⁻¹ = (a⁻¹)⁻¹ * 1 := by simp _ = (a⁻¹)⁻¹ * (a⁻¹ * a) := by simp _ = ((a⁻¹)⁻¹ * a⁻¹) * a := by simp _ = 1 * a := by simp _ = a := by simp -- 4ª demostración -- =============== example : (a⁻¹)⁻¹ = a := by apply mul_eq_one_iff_inv_eq.mp -- ⊢ a⁻¹ * a = 1 exact mul_left_inv a -- 5ª demostración -- =============== example : (a⁻¹)⁻¹ = a := mul_eq_one_iff_inv_eq.mp (mul_left_inv a) -- 6ª demostración -- =============== example : (a⁻¹)⁻¹ = a:= inv_inv a -- 7ª demostración -- =============== example : (a⁻¹)⁻¹ = a:= by simp -- Lemas usados -- ============ -- variable (b c : G) -- #check (inv_inv a : (a⁻¹)⁻¹ = a) -- #check (inv_mul_self a : a⁻¹ * a = 1) -- #check (mul_assoc a b c : (a * b) * c = a * (b * c)) -- #check (mul_eq_one_iff_inv_eq : a * b = 1 ↔ a⁻¹ = b) -- #check (mul_left_inv a : a⁻¹ * a = 1) -- #check (mul_one a : a * 1 = a) -- #check (one_mul a : 1 * a = a) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones con Isabelle/HOL
|
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 67 68 69 70 71 |
theory Inverso_del_inverso_en_grupos imports Main begin context group begin (* 1ª demostración *) lemma "inverse (inverse a) = a" proof - have "inverse (inverse a) = (inverse (inverse a)) * 1" by (simp only: right_neutral) also have "… = inverse (inverse a) * (inverse a * a)" by (simp only: left_inverse) also have "… = (inverse (inverse a) * inverse a) * a" by (simp only: assoc) also have "… = 1 * a" by (simp only: left_inverse) also have "… = a" by (simp only: left_neutral) finally show "inverse (inverse a) = a" by this qed (* 2ª demostración *) lemma "inverse (inverse a) = a" proof - have "inverse (inverse a) = (inverse (inverse a)) * 1" by simp also have "… = inverse (inverse a) * (inverse a * a)" by simp also have "… = (inverse (inverse a) * inverse a) * a" by simp also have "… = 1 * a" by simp finally show "inverse (inverse a) = a" by simp qed (* 3ª demostración *) lemma "inverse (inverse a) = a" proof (rule inverse_unique) show "inverse a * a = 1" by (simp only: left_inverse) qed (* 4ª demostración *) lemma "inverse (inverse a) = a" proof (rule inverse_unique) show "inverse a * a = 1" by simp qed (* 5ª demostración *) lemma "inverse (inverse a) = a" by (rule inverse_unique) simp (* 6ª demostración *) lemma "inverse (inverse a) = a" by (simp only: inverse_inverse) (* 7ª demostración *) lemma "inverse (inverse a) = a" by simp end end |
