Demostrar 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 * b = 1, entonces a\u207b\u00b9 = b.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport algebra.group.basic\n\nuniverse u\nvariables {G : Type u} [group G]\nvariables {a b : G}\n\nexample\n (h : a * b = 1)\n : a\u207b\u00b9 = b :=\nsorry\n<\/pre>\n[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n
\r\nimport algebra.group.basic\r\n\r\nuniverse u\r\nvariables {G : Type u} [group G]\r\nvariables {a b : G}\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : a * b = 1)\r\n : a\u207b\u00b9 = b :=\r\ncalc a\u207b\u00b9 = a\u207b\u00b9 * 1 : (mul_one a\u207b\u00b9).symm\r\n ... = a\u207b\u00b9 * (a * b) : congr_arg ((*) a\u207b\u00b9) h.symm\r\n ... = (a\u207b\u00b9 * a) * b : (mul_assoc a\u207b\u00b9 a b).symm\r\n ... = 1 * b : congr_arg (* b) (inv_mul_self a)\r\n ... = b : one_mul b\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : a * b = 1)\r\n : a\u207b\u00b9 = b :=\r\ncalc a\u207b\u00b9 = a\u207b\u00b9 * 1 : by simp only [mul_one]\r\n ... = a\u207b\u00b9 * (a * b) : by simp only [h]\r\n ... = (a\u207b\u00b9 * a) * b : by simp only [mul_assoc]\r\n ... = 1 * b : by simp only [inv_mul_self]\r\n ... = b : by simp only [one_mul]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : a * b = 1)\r\n : a\u207b\u00b9 = b :=\r\ncalc 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-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : a * b = 1)\r\n : a\u207b\u00b9 = b :=\r\ncalc a\u207b\u00b9 = a\u207b\u00b9 * (a * b) : by simp [h]\r\n ... = b : by simp\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : b * a = 1)\r\n : b = a\u207b\u00b9 :=\r\neq_inv_of_mul_eq_one h\r\n<\/pre>\n