Producto_por_uno.md

Título	Autor
Si G es un grupo y a ∈ G, entonces a·1 = a	José A. Alonso

Demostrar con Lean4 que si (G) es un grupo y (a \in G), entonces [a·1 = a]

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]
variable (a b : G)

example : a * 1 = a :=
sorry

Demostración en lenguaje natural

[mathjax] Se tiene por la siguiente cadena de igualdades \begin{align} a·1 &= a·(a⁻¹·a) &&\text{[por producto con inverso]} \ &= (a·a⁻¹)·a &&\text{[por asociativa]} \ &= 1·a &&\text{[por producto con inverso]} \ &= a &&\text{[por producto con uno]} \end{align}

Demostraciones con Lean4

import Mathlib.Algebra.Group.Defs

variable {G : Type _} [Group G]
variable (a b : G)

-- 1ª demostración
example : a * 1 = a :=
calc
  a * 1 = a * (a⁻¹ * a) := by rw [mul_left_inv]
      _ = (a * a⁻¹) * a := by rw [mul_assoc]
      _ = 1 * a         := by rw [mul_right_inv]
      _ = a             := by rw [one_mul]

-- 2ª demostración
example : a * 1 = a :=
calc
  a * 1 = a * (a⁻¹ * a) := by simp
      _ = (a * a⁻¹) * a := by simp
      _ = 1 * a         := by simp
      _ = a             := by simp

-- 3ª demostración
example : a * 1 = a :=
by simp

-- 4ª demostración
example : a * 1 = a :=
by exact mul_one a

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias

• J. Avigad y P. Massot. Mathematics in Lean, p. 12.