Si G es un grupo y a ∈ G, entonces a * 1 = a
Demostrar que si G es un grupo y a ∈ G, entonces
1 |
a * 1 = a |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 |
import algebra.group variables {G : Type*} [group G] variables a : G example : a * 1 = a := sorry |