En Lean4, se declara que \\(G\\) es un grupo mediante la expresi\u00f3n<\/p>\n
\r\n variable {G : Type _} [Group G]\r\n<\/pre>\nComo consecuencia, se tiene los siguientes axiomas<\/p>\n
\r\n mul_assoc : \u2200 a b c : G, a * b * c = a * (b * c)\r\n one_mul : \u2200 a : G, 1 * a = a\r\n mul_left_inv : \u2200 a : G, a\u207b\u00b9 * a = 1\r\n<\/pre>\nDemostrar que si \\(G\\) es un grupo y \\(a \\in G\\), entonces
\n\\[aa\u207b\u00b9 = 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 * a\u207b\u00b9 = 1 :=\r\nsorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nPor la siguiente cadena de igualdades
\n\\begin{align}
\n a\u00b7a\u207b\u00b9 &= 1\u00b7(a\u00b7a\u207b\u00b9) &&\\text{[por producto con uno]} \\\\
\n &= (1\u00b7a)\u00b7a\u207b\u00b9 &&\\text{[por asociativa]} \\\\
\n &= (((a\u207b\u00b9)\u207b\u00b9\u00b7a\u207b\u00b9) \u00b7a)\u00b7a\u207b\u00b9 &&\\text{[por producto con inverso]} \\\\
\n &= ((a\u207b\u00b9)\u207b\u00b9\u00b7(a\u207b\u00b9 \u00b7a))\u00b7a\u207b\u00b9 &&\\text{[por asociativa]} \\\\
\n &= ((a\u207b\u00b9)\u207b\u00b9\u00b71)\u00b7a\u207b\u00b9 &&\\text{[por producto con inverso]} \\\\
\n &= (a\u207b\u00b9)\u207b\u00b9\u00b7(1\u00b7a\u207b\u00b9) &&\\text{[por asociativa]} \\\\
\n &= (a\u207b\u00b9)\u207b\u00b9\u00b7a\u207b\u00b9 &&\\text{[por producto con uno]} \\\\
\n &= 1 &&\\text{[por producto con 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\n-- 1\u00aa demostraci\u00f3n\r\nexample : a * a\u207b\u00b9 = 1 :=\r\ncalc\r\n a * a\u207b\u00b9 = 1 * (a * a\u207b\u00b9) := by rw [one_mul]\r\n _ = (1 * a) * a\u207b\u00b9 := by rw [mul_assoc]\r\n _ = (((a\u207b\u00b9)\u207b\u00b9 * a\u207b\u00b9) * a) * a\u207b\u00b9 := by rw [mul_left_inv]\r\n _ = ((a\u207b\u00b9)\u207b\u00b9 * (a\u207b\u00b9 * a)) * a\u207b\u00b9 := by rw [\u2190 mul_assoc]\r\n _ = ((a\u207b\u00b9)\u207b\u00b9 * 1) * a\u207b\u00b9 := by rw [mul_left_inv]\r\n _ = (a\u207b\u00b9)\u207b\u00b9 * (1 * a\u207b\u00b9) := by rw [mul_assoc]\r\n _ = (a\u207b\u00b9)\u207b\u00b9 * a\u207b\u00b9 := by rw [one_mul]\r\n _ = 1 := by rw [mul_left_inv]\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample : a * a\u207b\u00b9 = 1 :=\r\ncalc\r\n a * a\u207b\u00b9 = 1 * (a * a\u207b\u00b9) := by simp\r\n _ = (1 * a) * a\u207b\u00b9 := by simp\r\n _ = (((a\u207b\u00b9)\u207b\u00b9 * a\u207b\u00b9) * a) * a\u207b\u00b9 := by simp\r\n _ = ((a\u207b\u00b9)\u207b\u00b9 * (a\u207b\u00b9 * a)) * a\u207b\u00b9 := by simp\r\n _ = ((a\u207b\u00b9)\u207b\u00b9 * 1) * a\u207b\u00b9 := by simp\r\n _ = (a\u207b\u00b9)\u207b\u00b9 * (1 * a\u207b\u00b9) := by simp\r\n _ = (a\u207b\u00b9)\u207b\u00b9 * a\u207b\u00b9 := by simp\r\n _ = 1 := by simp\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : a * a\u207b\u00b9 = 1 :=\r\nby simp\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample : a * a\u207b\u00b9 = 1 :=\r\nby exact mul_inv_self a\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