{"id":1032,"date":"2022-09-15T06:00:31","date_gmt":"2022-09-15T04:00:31","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1032"},"modified":"2022-09-11T16:27:59","modified_gmt":"2022-09-11T14:27:59","slug":"si-g-es-un-grupo-y-a-%e2%88%88-g-entonces-a-1-a","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/si-g-es-un-grupo-y-a-%e2%88%88-g-entonces-a-1-a\/","title":{"rendered":"Si G es un grupo y a \u2208 G, entonces a * 1 = a"},"content":{"rendered":"

Demostrar que si G es un grupo y a \u2208 G, entonces<\/p>\n

\na * 1 = a\n<\/pre>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport algebra.group\nvariables {G : Type*} [group G]\nvariables a : G\n\nexample : a * 1 = a :=\nsorry\n<\/pre>\n
<\/p>\n
Soluciones con Lean<\/b><\/p>\n
\nimport algebra.group\nvariables {G : Type*} [group G]\nvariables a : G\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 1 = a :=\ncalc\n  a * 1 = a * (a\u207b\u00b9 * a) : congr_arg (\u03bb x, a * x) (mul_left_inv a).symm\n    ... = (a * a\u207b\u00b9) * a : (mul_assoc a a\u207b\u00b9 a).symm\n    ... = 1 * a         : congr_arg (\u03bb x, x* a) (mul_right_inv a)\n    ... = a             : one_mul a\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 1 = a :=\ncalc\n  a * 1 = a * (a\u207b\u00b9 * a) : by rw mul_left_inv\n    ... = (a * a\u207b\u00b9) * a : by rw mul_assoc\n    ... = 1 * a         : by rw mul_right_inv\n    ... = a             : by rw one_mul\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 1 = a :=\ncalc\n  a * 1 = a * (a\u207b\u00b9 * a) : by simp\n    ... = (a * a\u207b\u00b9) * a : by simp\n    ... = 1 * a         : by simp\n    ... = a             : by simp\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 1 = a :=\nby simp\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a * 1 = a :=\n-- by library_search\nmul_one a\n<\/pre>\n
Se puede interactuar con la prueba anterior en esta sesi\u00f3n con Lean<\/a>.<\/p>\n
Referencias<\/b><\/p>\n