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
1 |
variables {G : Type*} [group G] |
y, como consecuencia, se tiene los siguientes axiomas
1 2 3 |
mul_assoc : ∀ a b c : G, a * b * c = a * (b * c) one_mul : ∀ a : G, 1 * a = a mul_left_inv : ∀ a : G, a⁻¹ * a = 1 |
Demostrar que si G es un grupo y a ∈ G, entonces
1 |
a * a⁻¹ = 1 |
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 b : G) example : a * a⁻¹ = 1 := sorry |