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 |