Si G es un grupo y a ∈ G, entonces a * a⁻¹ = 1

En Lean, se declara que G es un grupo mediante la expresión

y, como consecuencia, se tiene los siguientes axiomas

Demostrar que si G es un grupo y a ∈ G, entonces

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

Read More «Si G es un grupo y a ∈ G, entonces a * a⁻¹ = 1»