Si G un grupo y a ∈ G, entonces (a⁻¹)⁻¹ = a
Demostrar con Lean4 que si \(G\) un grupo y \(a ∈ G\), entonces
\[(a⁻¹)⁻¹ = a\]
Para ello, completar la siguiente teoría de Lean4:
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] variable {a : G} example : (a⁻¹)⁻¹ = a := sorry |