Unicidad de los inversos en los grupos
Demostrar con Lean4 que si \(a\) es un elemento de un grupo \(G\), entonces \(a\) tiene un único inverso; es decir, si \(b\) es un elemento de \(G\) tal que \(a·b = 1\), entonces \(a⁻¹ = b\).
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] variable {a b : G} example (h : a * b = 1) : a⁻¹ = b := by sorry |