Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹
Demostrar con Lean4 que si \(G\) es un grupo y \(a, b \in G\), entonces \((ab)^{-1} = b^{-1}a^{-1}\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Group.Defs variable {G : Type _} [Group G] variable (a b : G) example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := sorry |
Demostración en lenguaje natural
Teniendo en cuenta la propiedad
\[(∀ a, b ∈ G)[ab = 1 → a⁻¹ = b] \]
basta demostrar que
\[(a·b)·(b⁻¹·a⁻¹) = 1.\]
que se demuestra mediante la siguiente cadena de igualdades
\begin{align}
(a·b)·(b⁻¹·a⁻¹) &= a·(b·(b⁻¹·a⁻¹)) &&\text{[por la asociativa]} \\
&= a·((b·b⁻¹)·a⁻¹) &&\text{[por la asociativa]} \\
&= a·(1·a⁻¹) &&\text{[por producto con inverso]} \\
&= a·a⁻¹ &&\text{[por producto con uno]} \\
&= 1 &&\text{[por producto con
inverso]}
\end{align}
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 |
import Mathlib.Algebra.Group.Defs variable {G : Type _} [Group G] variable (a b : G) lemma aux : (a * b) * (b⁻¹ * a⁻¹) = 1 := calc (a * b) * (b⁻¹ * a⁻¹) = a * (b * (b⁻¹ * a⁻¹)) := by rw [mul_assoc] _ = a * ((b * b⁻¹) * a⁻¹) := by rw [mul_assoc] _ = a * (1 * a⁻¹) := by rw [mul_right_inv] _ = a * a⁻¹ := by rw [one_mul] _ = 1 := by rw [mul_right_inv] -- 1ª demostración example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by have h1 : (a * b) * (b⁻¹ * a⁻¹) = 1 := aux a b show (a * b)⁻¹ = b⁻¹ * a⁻¹ exact inv_eq_of_mul_eq_one_right h1 -- 3ª demostración example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by have h1 : (a * b) * (b⁻¹ * a⁻¹) = 1 := aux a b show (a * b)⁻¹ = b⁻¹ * a⁻¹ simp [h1] -- 4ª demostración example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by have h1 : (a * b) * (b⁻¹ * a⁻¹) = 1 := aux a b simp [h1] -- 5ª demostración example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by apply inv_eq_of_mul_eq_one_right rw [aux] -- 6ª demostración example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by exact mul_inv_rev a b -- 7ª demostración example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by simp |
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 |
theory Inverso_del_producto imports Main begin context group begin (* 1ª demostración *) lemma "inverse (a * b) = inverse b * inverse a" proof (rule inverse_unique) have "(a * b) * (inverse b * inverse a) = ((a * b) * inverse b) * inverse a" by (simp only: assoc) also have "… = (a * (b * inverse b)) * inverse a" by (simp only: assoc) also have "… = (a * 1) * inverse a" by (simp only: right_inverse) also have "… = a * inverse a" by (simp only: right_neutral) also have "… = 1" by (simp only: right_inverse) finally show "a * b * (inverse b * inverse a) = 1" by this qed (* 2ª demostración *) lemma "inverse (a * b) = inverse b * inverse a" proof (rule inverse_unique) have "(a * b) * (inverse b * inverse a) = ((a * b) * inverse b) * inverse a" by (simp only: assoc) also have "… = (a * (b * inverse b)) * inverse a" by (simp only: assoc) also have "… = (a * 1) * inverse a" by simp also have "… = a * inverse a" by simp also have "… = 1" by simp finally show "a * b * (inverse b * inverse a) = 1" . qed (* 3ª demostración *) lemma "inverse (a * b) = inverse b * inverse a" proof (rule inverse_unique) have "a * b * (inverse b * inverse a) = a * (b * inverse b) * inverse a" by (simp only: assoc) also have "… = 1" by simp finally show "a * b * (inverse b * inverse a) = 1" . qed (* 4ª demostración *) lemma "inverse (a * b) = inverse b * inverse a" by (simp only: inverse_distrib_swap) end end |
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 12.
