Si G es un grupo y a, b ∈ G tales que b * a = 1, entonces a⁻¹ = b
Demostrar que si G es un grupo y a, b ∈ G tales que
|
1 |
b * a = 1 |
entonces
|
1 |
a⁻¹ = b |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 |
import algebra.group variables {G : Type*} [group G] variables a b : G example (h : b * a = 1) : a⁻¹ = b := sorry |
Read More «Si G es un grupo y a, b ∈ G tales que b * a = 1, entonces a⁻¹ = b»