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
\r\nimport Mathlib.Algebra.Group.Defs\r\n\r\nvariable {G : Type _} [Group G]\r\nvariable (a b : G)\r\n\r\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\r\nsorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nTeniendo en cuenta la propiedad
\n \\[\u2200 a\\ b \u2208 R, ab = 1 \u2192 a\u207b\u00b9 = b,\\]
\nbasta demostrar que
\n \\[(a\u00b7b)\u00b7(b\u207b\u00b9\u00b7a\u207b\u00b9) = 1.\\]
\nLa identidad anterior 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<\/b><\/p>\n\r\nimport Mathlib.Algebra.Group.Defs\r\n\r\nvariable {G : Type _} [Group G]\r\nvariable (a b : G)\r\n\r\nlemma aux : (a * b) * (b\u207b\u00b9 * a\u207b\u00b9) = 1 :=\r\ncalc\r\n (a * b) * (b\u207b\u00b9 * a\u207b\u00b9)\r\n = a * (b * (b\u207b\u00b9 * a\u207b\u00b9)) := by rw [mul_assoc]\r\n _ = a * ((b * b\u207b\u00b9) * a\u207b\u00b9) := by rw [mul_assoc]\r\n _ = a * (1 * a\u207b\u00b9) := by rw [mul_right_inv]\r\n _ = a * a\u207b\u00b9 := by rw [one_mul]\r\n _ = 1 := by rw [mul_right_inv]\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\r\nby\r\n have h1 : (a * b) * (b\u207b\u00b9 * a\u207b\u00b9) = 1 :=\r\n aux a b\r\n show (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9\r\n exact inv_eq_of_mul_eq_one_right h1\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\r\nby\r\n have h1 : (a * b) * (b\u207b\u00b9 * a\u207b\u00b9) = 1 :=\r\n aux a b\r\n show (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9\r\n simp [h1]\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\r\nby\r\n have h1 : (a * b) * (b\u207b\u00b9 * a\u207b\u00b9) = 1 :=\r\n aux a b\r\n simp [h1]\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\r\nby\r\n apply inv_eq_of_mul_eq_one_right\r\n rw [aux]\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\r\nby exact mul_inv_rev a b\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\nexample : (a * b)\u207b\u00b9 = b\u207b\u00b9 * a\u207b\u00b9 :=\r\nby simp\r\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n