Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹

Demostrar con Lean4 que si \(G\) es un grupo y \(a, b \in G\), entonces \((ab)^{-1} = b^{-1}a^{-1}\).

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

Demostración en lenguaje natural


Teniendo en cuenta la propiedad
\[(∀ a, b ∈ G)[ab = 1 → a⁻¹ = b] \]
basta demostrar que
\[(a·b)·(b⁻¹·a⁻¹) = 1.\]
que se demuestra mediante la siguiente cadena de igualdades
\begin{align}
(a·b)·(b⁻¹·a⁻¹) &= a·(b·(b⁻¹·a⁻¹)) &&\text{[por la asociativa]} \\
&= a·((b·b⁻¹)·a⁻¹) &&\text{[por la asociativa]} \\
&= a·(1·a⁻¹) &&\text{[por producto con inverso]} \\
&= a·a⁻¹ &&\text{[por producto con uno]} \\
&= 1 &&\text{[por producto con
inverso]}
\end{align}

Demostraciones con Lean4

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

Referencias

Escribe un comentario