{"id":2463,"date":"2024-05-10T06:00:24","date_gmt":"2024-05-10T04:00:24","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=2463"},"modified":"2024-05-09T13:05:59","modified_gmt":"2024-05-09T11:05:59","slug":"10-may-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/10-may-24\/","title":{"rendered":"Unicidad del elemento neutro en los grupos"},"content":{"rendered":"\n

Demostrar con Lean4 que un grupo solo posee un elemento neutro.<\/p>\n

Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n

\nimport Mathlib.Algebra.Group.Basic\n\nvariable {G : Type} [Group G]\n\nexample\n  (e : G)\n  (h : \u2200 x, x * e = x)\n  : e = 1 :=\nsorry\n<\/pre>\n
<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(e \u2208 G\) tal que
\n\[ (\u2200 x)[x\u00b7e = x] \tag{1} \]
\nEntonces,
\n\begin{align}
\n   e &= 1.e    &&\text{[porque 1 es neutro]} \\
\n     &= 1      &&\text{[por (1)]}
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n
\nimport Mathlib.Algebra.Group.Basic\n\nvariable {G : Type} [Group G]\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (e : G)\n  (h : \u2200 x, x * e = x)\n  : e = 1 :=\ncalc e = 1 * e := (one_mul e).symm\n     _ = 1     := h 1\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (e : G)\n  (h : \u2200 x, x * e = x)\n  : e = 1 :=\nby\n  have h1 : e = e * e := (h e).symm\n  exact self_eq_mul_left.mp h1\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (e : G)\n  (h : \u2200 x, x * e = x)\n  : e = 1 :=\nself_eq_mul_left.mp (h e).symm\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (e : G)\n  (h : \u2200 x, x * e = x)\n  : e = 1 :=\nby aesop\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : G)\n-- #check (one_mul a : 1 * a = a)\n-- #check (self_eq_mul_left : b = a * b \u2194 a = 1)\n<\/pre>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
3. Demostraciones con Isabelle\/HOL<\/h2>\n
\ntheory Unicidad_del_elemento_neutro_en_los_grupos\nimports Main\nbegin\n\ncontext group\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"\u2200 x. x * e = x\"\n  shows   \"e = 1\"\nproof -\n  have \"e = 1 * e\"     by (simp only: left_neutral)\n  also have \"\u2026 = 1\"    using assms by (rule allE)\n  finally show \"e = 1\" by this\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"\u2200 x. x * e = x\"\n  shows   \"e = 1\"\nproof -\n  have \"e = 1 * e\"     by simp\n  also have \"\u2026 = 1\"    using assms by simp\n  finally show \"e = 1\" .\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"\u2200 x. x * e = x\"\n  shows   \"e = 1\"\n  using assms\n  by (metis left_neutral)\n\nend\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"
Demostrar con Lean4 que un grupo solo posee un elemento neutro. Para ello, completar la siguiente teor\u00eda de Lean4: import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] example (e : G) (h : \u2200 x, x * e = x) : e = 1 := sorry<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"default","_kad_post_title":"default","_kad_post_layout":"default","_kad_post_sidebar_id":"","_kad_post_content_style":"default","_kad_post_vertical_padding":"default","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[11],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2463"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=2463"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2463\/revisions"}],"predecessor-version":[{"id":2465,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2463\/revisions\/2465"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=2463"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=2463"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=2463"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}