Unicidad del elemento neutro en los grupos
Demostrar que un grupo sólo posee un elemento neutro.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 |
import algebra.group.basic universe u variables {G : Type u} [group G] example (e : G) (h : ∀ x, x * e = x) : e = 1 := sorry |
[expand title=»Soluciones con Lean»]
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 |
import algebra.group.basic universe u variables {G : Type u} [group G] -- 1ª demostración -- =============== example (e : G) (h : ∀ x, x * e = x) : e = 1 := calc e = 1 * e : (one_mul e).symm ... = 1 : h 1 -- 2ª demostración -- =============== example (e : G) (h : ∀ x, x * e = x) : e = 1 := by finish |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]
[expand title=»Soluciones con Isabelle/HOL»]
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 |
theory Unicidad_del_elemento_neutro_en_los_grupos imports Main begin context group begin (* 1ª demostración *) lemma assumes "∀ x. x * e = x" shows "e = 1" proof - have "e = 1 * e" by (simp only: left_neutral) also have "… = 1" using assms by (rule allE) finally show "e = 1" by this qed (* 2ª demostración *) lemma assumes "∀ x. x * e = x" shows "e = 1" proof - have "e = 1 * e" by simp also have "… = 1" using assms by simp finally show "e = 1" . qed (* 3ª demostración *) lemma assumes "∀ x. x * e = x" shows "e = 1" using assms by (metis left_neutral) end end |
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]
Referencia
Propiedad 3.17 del libro Abstract algebra: Theory and applications de Thomas W. Judson.