Unicidad del elemento neutro en los grupos
Demostrar con Lean4 que un grupo solo posee un elemento neutro.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] example (e : G) (h : ∀ x, x * e = x) : e = 1 := sorry |
1. Demostración en lenguaje natural
Sea \(e ∈ G\) tal que
\[ (∀ x)[x·e = x] \tag{1} \]
Entonces,
\begin{align}
e &= 1.e &&\text{[porque 1 es neutro]} \\
&= 1 &&\text{[por (1)]}
\end{align}
2. Demostraciones con Lean4
|
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 41 42 43 44 45 46 47 48 49 |
import Mathlib.Algebra.Group.Basic variable {G : Type} [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 have h1 : e = e * e := (h e).symm exact self_eq_mul_left.mp h1 -- 3ª demostración -- =============== example (e : G) (h : ∀ x, x * e = x) : e = 1 := self_eq_mul_left.mp (h e).symm -- 4ª demostración -- =============== example (e : G) (h : ∀ x, x * e = x) : e = 1 := by aesop -- Lemas usados -- ============ -- variable (a b : G) -- #check (one_mul a : 1 * a = a) -- #check (self_eq_mul_left : b = a * b ↔ a = 1) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones 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 |
