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:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Group.Defs variable {G : Type _} [Group G] variable (a b : G) example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := sorry |
Read More «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\) tales que \(ab = 1\) entonces \(a^{-1} = b\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Algebra.Group.Defs variable {G : Type _} [Group G] variable (a b : G) example (h : a * b = 1) : a⁻¹ = b := sorry |
Read More «Si G es un grupo y a, b ∈ G, tales que ab = 1 entonces a⁻¹ = b»
Demostrar que si G es un grupo y a, b ∈ G, entonces
|
1 |
(a * b)⁻¹ = b⁻¹ * 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 b : G example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := sorry |
Read More «Si G es un grupo y a, b ∈ G, entonces (a * b)⁻¹ = b⁻¹ * a⁻¹»
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»
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 |