Demostrar con Lean4 que si \(G\) es un grupo y \(a, b \in G\), entonces \((ab)^{-1} = b^{-1}a^{-1}\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Algebra.Group.Defs\n\nvariable {G : Type _} [Group G]\nvariable (a b : G)\n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nsorry\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/h2>\n
\nTeniendo en cuenta la propiedad
\n \[(\u2200 a, b \u2208 G)[ab = 1 \u2192 a\u207b\u00b9 = b] \]
\nbasta demostrar que
\n \[(a\u00b7b)\u00b7(b\u207b\u00b9\u00b7a\u207b\u00b9) = 1.\]
\nque se demuestra mediante la siguiente cadena de igualdades
\n\begin{align}
\n (a\u00b7b)\u00b7(b\u207b\u00b9\u00b7a\u207b\u00b9) &= a\u00b7(b\u00b7(b\u207b\u00b9\u00b7a\u207b\u00b9)) &&\text{[por la asociativa]} \\
\n &= a\u00b7((b\u00b7b\u207b\u00b9)\u00b7a\u207b\u00b9) &&\text{[por la asociativa]} \\
\n &= a\u00b7(1\u00b7a\u207b\u00b9) &&\text{[por producto con inverso]} \\
\n &= a\u00b7a\u207b\u00b9 &&\text{[por producto con uno]} \\
\n &= 1 &&\text{[por producto con
\n inverso]}
\n\end{align}<\/p>\n
Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Algebra.Group.Defs\n\nvariable {G : Type _} [Group G]\nvariable (a b : G)\n\nlemma aux : (a * b) * (b\u207b\u00b9 * a\u207b\u00b9) = 1 :=\ncalc\n (a * b) * (b\u207b\u00b9 * a\u207b\u00b9)\n = a * (b * (b\u207b\u00b9 * a\u207b\u00b9)) := by rw [mul_assoc]\n _ = a * ((b * b\u207b\u00b9) * a\u207b\u00b9) := by rw [mul_assoc]\n _ = a * (1 * a\u207b\u00b9) := by rw [mul_right_inv]\n _ = a * a\u207b\u00b9 := by rw [one_mul]\n _ = 1 := by rw [mul_right_inv]\n\n-- 1\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby\n have h1 : (a * b) * (b\u207b\u00b9 * a\u207b\u00b9) = 1 :=\n aux a b\n show (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9\n exact inv_eq_of_mul_eq_one_right h1\n\n-- 3\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby\n have h1 : (a * b) * (b\u207b\u00b9 * a\u207b\u00b9) = 1 :=\n aux a b\n show (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9\n simp [h1]\n\n-- 4\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby\n have h1 : (a * b) * (b\u207b\u00b9 * a\u207b\u00b9) = 1 :=\n aux a b\n simp [h1]\n\n-- 5\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby\n apply inv_eq_of_mul_eq_one_right\n rw [aux]\n\n-- 6\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby exact mul_inv_rev a b\n\n-- 7\u00aa demostraci\u00f3n\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\nby simp\n<\/pre>\n