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:

Read More «Si G un grupo y a ∈ G, entonces (a⁻¹)⁻¹ = a»