Demostrar con Lean4 que si M es un monoide, a∈M y m,n∈ℕ, entonces
am·n=(am)n
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Algebra.GroupPower.Basic open Nat variable {M : Type} [Monoid M] variable (a : M) variable (m n : ℕ) example : a^(m * n) = (a^m)^n := by sorry |
Read More «Si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces a^(m·n) = (a^m)^n»
Demostrar con Lean4 que si G es un grupo y a,b,c∈G tales que a·b=a·c, entonces b=c.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] variable {a b c : G} example (h: a * b = a * c) : b = c := sorry |
Read More «Si G es un grupo y a, b, c ∈ G tales que a·b = a·c, entonces b = c»
Demostrar con Lean4 que si G un grupo y a∈G, entonces
(a⁻¹)⁻¹=a
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] variable {a : G} example : (a⁻¹)⁻¹ = a := sorry |
Demostrar con Lean4 que si G es un grupo y a,b∈G, entonces (ab)−1=b−1a−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 a es un elemento de un grupo G, entonces a tiene un único inverso; es decir, si b es un elemento de G tal que a·b=1, entonces a⁻¹=b.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] variable {a b : G} example (h : a * b = 1) : a⁻¹ = b := by sorry |
Demostrar con Lean4 que un grupo solo posee un elemento neutro.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] example (e : G) (h : ∀ x, x * e = x) : e = 1 := sorry |
Un monoide cancelativo por la izquierda es un monoide M que cumple la propiedad cancelativa por la izquierda; es decir, para todo a,b∈M
a·b=a·c↔b=c
En Lean4 la clase de los monoides cancelativos por la izquierda es LeftCancelMonoid y la propiedad cancelativa por la izquierda es
|
1 |
mul_left_cancel : a * b = a * c → b = c |
Demostrar con Lean4 que si M es un monoide cancelativo por la izquierda y a,b∈M, entonces
a·b=a↔b=1
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Group.Basic variable {M : Type} [LeftCancelMonoid M] variable {a b : M} example : a * b = a ↔ b = 1 := by sorry |
Read More «Caracterización de producto igual al primer factor»
Demostrar con Lean4 que si M es un monoide conmutativo y x,y,z∈M tales que x·y=1 y x·z=1, entonces y=z.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Algebra.Group.Basic variable {M : Type} [CommMonoid M] variable {x y z : M} example (hy : x * y = 1) (hz : x * z = 1) : y = z := by sorry |
Sea M un monoide y a,b∈M tales que ab=1. Demostrar con Lean4 que a=1 si y sólo si b=1.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Algebra.Group.Basic variable {M : Type} [Monoid M] variable {a b : M} example (h : a * b = 1) : a = 1 ↔ b = 1 := by sorry |
En los monoides se define la potencia con exponentes naturales. En Lean la potencia x^n se se caracteriza por los siguientes lemas:
|
1 2 |
pow_zero : x^0 = 1 pow_succ : x^(succ n) = x * x^n |
Demostrar con Lean4 que si M es un monoide, x∈M y m,n∈ℕ, entonces
xm+n=xmxn
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 |
import Mathlib.Algebra.Group.Defs import Mathlib.Algebra.GroupPower.Basic open Nat variable {M : Type} [Monoid M] variable (x : M) variable (m n : ℕ) example : x^(m + n) = x^m * x^n := by sorry |
Read More «Producto de potencias de la misma base en monoides»