Demostrar con Lean4 que si \\(G\\) es un grupo y \\(a, b \\in G\\) tales que \\(ab = 1\\) entonces \\(a^{-1} = b\\).<\/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\r\n (h : a * b = 1)\r\n : a\u207b\u00b9 = b :=\r\nsorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nSe tiene a partir de la siguente cadena de igualdades
\n\\begin{align}
\n a\u207b\u00b9 &= a\u207b\u00b9\u00b71 &&\\text{[por producto por uno]} \\\\
\n &= a\u207b\u00b9\u00b7(a\u00b7b) &&\\text{[por hip\u00f3tesis]} \\\\
\n &= (a\u207b\u00b9\u00b7a)\u00b7b &&\\text{[por asociativa]} \\\\
\n &= 1\u00b7b &&\\text{[por producto con inverso]} \\\\
\n &= b &&\\text{[por producto por uno]}
\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\u00ba demostraci\u00f3n\r\nexample\r\n (h : a * b = 1)\r\n : a\u207b\u00b9 = b :=\r\ncalc\r\n a\u207b\u00b9 = a\u207b\u00b9 * 1 := by rw [mul_one]\r\n _ = a\u207b\u00b9 * (a * b) := by rw [h]\r\n _ = (a\u207b\u00b9 * a) * b := by rw [mul_assoc]\r\n _ = 1 * b := by rw [mul_left_inv]\r\n _ = b := by rw [one_mul]\r\n\r\n-- 2\u00ba demostraci\u00f3n\r\nexample\r\n (h : a * b = 1)\r\n : a\u207b\u00b9 = b :=\r\ncalc\r\n a\u207b\u00b9 = a\u207b\u00b9 * 1 := by simp\r\n _ = a\u207b\u00b9 * (a * b) := by simp [h]\r\n _ = (a\u207b\u00b9 * a) * b := by simp\r\n _ = 1 * b := by simp\r\n _ = b := by simp\r\n\r\n-- 3\u00ba demostraci\u00f3n\r\nexample\r\n (h : a * b = 1)\r\n : a\u207b\u00b9 = b :=\r\ncalc\r\n a\u207b\u00b9 = a\u207b\u00b9 * (a * b) := by simp [h]\r\n _ = b := by simp\r\n\r\n-- 4\u00ba demostraci\u00f3n\r\nexample\r\n (h : a * b = 1)\r\n : a\u207b\u00b9 = b :=\r\nby exact inv_eq_of_mul_eq_one_right h\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