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:
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
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:
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] variable {a b c : G} example (h: a * b = a * c) : b = c := sorry
Demostrar con Lean4 que si \(G\) un grupo y \(a ∈ G\), entonces \[(a⁻¹)⁻¹ = a\]
Para ello, completar la siguiente teoría de Lean4:
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:
import Mathlib.Algebra.Group.Defs variable {G : Type _} [Group G] variable (a b : G) example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := sorry
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:
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 sólo posee un elemento neutro.
Para ello, completar la siguiente teoría de Lean4:
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
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:
import Mathlib.Algebra.Group.Basic variable {M : Type} [LeftCancelMonoid M] variable {a b : M} example : a * b = a ↔ b = 1 := by sorry
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:
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:
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 dos siguientes lemas:
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:
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