Unicidad del elemento neutro en los grupos
Demostrar con Lean4 que un grupo sólo posee un elemento neutro.
Para ello, completar la siguiente teoría de Lean4:
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]} \newline &= 1 &&\text{[por (1)]} \end{align}
2. Demostraciones con Lean4
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
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