Demostrar con Lean4 que si \(a\) es un elemento de un grupo \(G\), entonces \(a\) tiene un \u00fanico inverso; es decir, si \(b\) es un elemento de \(G\) tal que \(a\u00b7b = 1\), entonces \(a\u207b\u00b9 = b\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Algebra.Group.Basic\n\nvariable {G : Type} [Group G]\nvariable {a b : G}\n\nexample\n (h : a * b = 1)\n : a\u207b\u00b9 = b :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Por la siguiente cadena de igualdades
\n\begin{align}
\n a\u207b\u00b9 &= a\u207b\u00b9\u00b71 &&\text{[porque 1 es neutro]} \\
\n &= a\u207b\u00b9\u00b7(a\u00b7b) &&\text{[por hip\u00f3tesis]} \\
\n &= (a\u207b\u00b9\u00b7a)\u00b7b &&\text{[por la asociativa]} \\
\n &= 1\u00b7b &&\text{[porque a\u207b\u00b9 es el inverso de a]} \\
\n &= b &&\text{[porque 1 es neutro]}
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Algebra.Group.Basic\n\nvariable {G : Type} [Group G]\nvariable {a b : G}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : a * b = 1)\n : a\u207b\u00b9 = b :=\ncalc a\u207b\u00b9 = a\u207b\u00b9 * 1 := (mul_one a\u207b\u00b9).symm\n _ = a\u207b\u00b9 * (a * b) := congrArg (a\u207b\u00b9 * .) h.symm\n _ = (a\u207b\u00b9 * a) * b := (mul_assoc a\u207b\u00b9 a b).symm\n _ = 1 * b := congrArg (. * b) (inv_mul_self a)\n _ = b := one_mul b\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : a * b = 1)\n : a\u207b\u00b9 = b :=\ncalc a\u207b\u00b9 = a\u207b\u00b9 * 1 := by simp only [mul_one]\n _ = a\u207b\u00b9 * (a * b) := by simp only [h]\n _ = (a\u207b\u00b9 * a) * b := by simp only [mul_assoc]\n _ = 1 * b := by simp only [inv_mul_self]\n _ = b := by simp only [one_mul]\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : a * b = 1)\n : a\u207b\u00b9 = b :=\ncalc a\u207b\u00b9 = a\u207b\u00b9 * 1 := by simp\n _ = a\u207b\u00b9 * (a * b) := by simp [h]\n _ = (a\u207b\u00b9 * a) * b := by simp\n _ = 1 * b := by simp\n _ = b := by simp\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : a * b = 1)\n : a\u207b\u00b9 = b :=\ncalc a\u207b\u00b9 = a\u207b\u00b9 * (a * b) := by simp [h]\n _ = b := by simp\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n (h : b * a = 1)\n : b = a\u207b\u00b9 :=\neq_inv_iff_mul_eq_one.mpr h\n\n-- Lemas usados\n-- ============\n\n-- variable (c : G)\n-- #check (eq_inv_iff_mul_eq_one : a = b\u207b\u00b9 \u2194 a * b = 1)\n-- #check (inv_mul_self a : a\u207b\u00b9 * a = 1)\n-- #check (mul_assoc a b c : (a * b) * c = a * (b * c))\n-- #check (mul_one a : a * 1 = a)\n-- #check (one_mul a : 1 * a = a)\n<\/pre>\n