Unicidad de los inversos en los grupos
Demostrar con Lean4 que si \(a\) es un elemento de un grupo \(G\), entonces \(a\) tiene un único inverso; es decir, si \(b\) es un elemento de \(G\) tal que \(a·b = 1\), entonces \(a⁻¹ = b\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] variable {a b : G} example (h : a * b = 1) : a⁻¹ = b := by 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·b) &&\text{[por hipótesis]} \\
&= (a⁻¹·a)·b &&\text{[por la asociativa]} \\
&= 1·b &&\text{[porque a⁻¹ es el inverso de a]} \\
&= b &&\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 |
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] variable {a b : G} -- 1ª demostración -- =============== example (h : a * b = 1) : a⁻¹ = b := calc a⁻¹ = a⁻¹ * 1 := (mul_one a⁻¹).symm _ = a⁻¹ * (a * b) := congrArg (a⁻¹ * .) h.symm _ = (a⁻¹ * a) * b := (mul_assoc a⁻¹ a b).symm _ = 1 * b := congrArg (. * b) (inv_mul_self a) _ = b := one_mul b -- 2ª demostración -- =============== example (h : a * b = 1) : a⁻¹ = b := calc a⁻¹ = a⁻¹ * 1 := by simp only [mul_one] _ = a⁻¹ * (a * b) := by simp only [h] _ = (a⁻¹ * a) * b := by simp only [mul_assoc] _ = 1 * b := by simp only [inv_mul_self] _ = b := by simp only [one_mul] -- 3ª demostración -- =============== example (h : a * b = 1) : a⁻¹ = b := calc a⁻¹ = a⁻¹ * 1 := by simp _ = a⁻¹ * (a * b) := by simp [h] _ = (a⁻¹ * a) * b := by simp _ = 1 * b := by simp _ = b := by simp -- 4ª demostración -- =============== example (h : a * b = 1) : a⁻¹ = b := calc a⁻¹ = a⁻¹ * (a * b) := by simp [h] _ = b := by simp -- 5ª demostración -- =============== example (h : b * a = 1) : b = a⁻¹ := eq_inv_iff_mul_eq_one.mpr h -- Lemas usados -- ============ -- variable (c : G) -- #check (eq_inv_iff_mul_eq_one : a = b⁻¹ ↔ a * b = 1) -- #check (inv_mul_self a : a⁻¹ * a = 1) -- #check (mul_assoc a b c : (a * b) * c = a * (b * c)) -- #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 |
theory Unicidad_de_los_inversos_en_los_grupos imports Main begin context group begin (* 1ª demostración *) lemma assumes "a * b = 1" shows "inverse a = b" proof - have "inverse a = inverse a * 1" by (simp only: right_neutral) also have "… = inverse a * (a * b)" by (simp only: assms(1)) also have "… = (inverse a * a) * b" by (simp only: assoc [symmetric]) also have "… = 1 * b" by (simp only: left_inverse) also have "… = b" by (simp only: left_neutral) finally show "inverse a = b" by this qed (* 2ª demostración *) lemma assumes "a * b = 1" shows "inverse a = b" proof - have "inverse a = inverse a * 1" by simp also have "… = inverse a * (a * b)" using assms by simp also have "… = (inverse a * a) * b" by (simp add: assoc [symmetric]) also have "… = 1 * b" by simp also have "… = b" by simp finally show "inverse a = b" . qed (* 3ª demostración *) lemma assumes "a * b = 1" shows "inverse a = b" proof - from assms have "inverse a * (a * b) = inverse a" by simp then show "inverse a = b" by (simp add: assoc [symmetric]) qed (* 4ª demostración *) lemma assumes "a * b = 1" shows "inverse a = b" using assms by (simp only: inverse_unique) end end |
