Unicidad_del_elemento_neutro_en_los_grupos.md

title	date	category	has_math
Unicidad del elemento neutro en los grupos	2024-05-10 06:00:00 UTC+02:00	Grupos	true

[mathjax]

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]} \\ &= 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