Demostrar con Lean4 que si \(M\) es un monoide, \(a ∈ M\) y \(m, n ∈ ℕ\), entonces
\[ a^{m·n} = (a^m)^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 \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 \(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
\[ x^{m + n} = x^m x^n \]
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»