Producto de potencias de la misma base en monoides
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»