Si G es un grupo y a ∈ G, entonces aa⁻¹ = 1
En Lean4, se declara que \(G\) es un grupo mediante la expresión
|
1 |
variable {G : Type _} [Group G] |
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 \in G\), entonces
\[aa⁻¹ = 1\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Group.Defs variable {G : Type _} [Group G] variable (a b : G) example : a * a⁻¹ = 1 := sorry |