{"id":520,"date":"2021-07-04T06:00:52","date_gmt":"2021-07-04T04:00:52","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=520"},"modified":"2021-07-04T17:04:08","modified_gmt":"2021-07-04T15:04:08","slug":"unicidad-del-elemento-neutro-en-los-grupos","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/unicidad-del-elemento-neutro-en-los-grupos\/","title":{"rendered":"Unicidad del elemento neutro en los grupos"},"content":{"rendered":"

Demostrar que un grupo s\u00f3lo posee un elemento neutro.<\/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]\n\nexample\n  (e : G)\n  (h : \u2200 x, x * e = x)\n  : e = 1 :=\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\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (e : G)\r\n  (h : \u2200 x, x * e = x)\r\n  : e = 1 :=\r\ncalc e = 1 * e : (one_mul e).symm\r\n   ... = 1     : h 1\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n  (e : G)\r\n  (h : \u2200 x, x * e = x)\r\n  : e = 1 :=\r\nby finish\r\n<\/pre>\n
Se puede interactuar con la prueba anterior en esta sesi\u00f3n con Lean<\/a>.<\/p>\n
En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con <pre lang="lean"> y otra con <\/pre>
\n[\/expand]<\/p>\n
[expand title=\u00bbSoluciones con Isabelle\/HOL\u00bb]<\/p>\n
\r\ntheory Unicidad_del_elemento_neutro_en_los_grupos\r\nimports Main\r\nbegin\r\n\r\ncontext group\r\nbegin\r\n\r\n(* 1\u00aa demostraci\u00f3n *)\r\n\r\nlemma\r\n  assumes \"\u2200 x. x * e = x\"\r\n  shows   \"e = 1\"\r\nproof -\r\n  have \"e = 1 * e\"     by (simp only: left_neutral)\r\n  also have \"\u2026 = 1\"    using assms by (rule allE)\r\n  finally show \"e = 1\" by this\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n *)\r\n\r\nlemma\r\n  assumes \"\u2200 x. x * e = x\"\r\n  shows   \"e = 1\"\r\nproof -\r\n  have \"e = 1 * e\"     by simp\r\n  also have \"\u2026 = 1\"    using assms by simp\r\n  finally show \"e = 1\" .\r\nqed\r\n\r\n(* 3\u00aa demostraci\u00f3n *)\r\n\r\nlemma\r\n  assumes \"\u2200 x. x * e = x\"\r\n  shows   \"e = 1\"\r\n  using assms\r\n  by (metis left_neutral)\r\n\r\nend\r\n\r\nend\r\n<\/pre>\n
En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con <pre lang="isar"> y otra con <\/pre>
\n[\/expand]<\/p>\n
 Referencia<\/h4>\n
Propiedad 3.17 del libro Abstract algebra: Theory and applications<\/a> de Thomas W. Judson.<\/p>\n","protected":false},"excerpt":{"rendered":"
Demostrar que un grupo s\u00f3lo posee un elemento neutro. Para ello, completar la siguiente teor\u00eda de Lean: import algebra.group.basic universe u variables {G : Type u} [group G] example (e : G) (h : \u2200 x, x * e = x) : e = 1 := sorry [expand title=\u00bbSoluciones con Lean\u00bb] import algebra.group.basic universe u variables {G : Type u} [group G] — 1\u00aa demostraci\u00f3n — =============== example (e : G) (h : \u2200 x, x * e = x) : e = 1 := calc e = 1 * e : (one_mul e).symm … = 1 : h 1 — 2\u00aa demostraci\u00f3n — =============== example (e : G) (h : \u2200 x, x * e = x) : e = 1 := by finish…<\/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":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_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\/520"}],"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=520"}],"version-history":[{"count":8,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/520\/revisions"}],"predecessor-version":[{"id":555,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/520\/revisions\/555"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=520"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=520"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=520"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}