---
title: Si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces a^(m·n) = (a^m)^n
date: 2024-05-17 06:00:00 UTC+02:00
category: Monoides
has_math: true
---
[mathjax]
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:
<pre lang="lean">
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
</pre>
<!--more-->
<h2>1. Demostración en lenguaje natural</h2>
Por inducción en \\(n\\).
**Caso base**: Supongamos que \\(n = 0\\). Entonces,
\\begin{align}
a^{m·0} &= a^0 \\\\
&= 1 &&\\text{[por pow_zero]} \\\\
&= (a^m)^0 &&\\text{[por pow_zero]}
\\end{align}
Paso de indución: Supogamos que se verifica para \\(n\\); es decir,
\\[ a^{m·n} = (a^m)^n \\tag{HI} \\]
Entonces,
\\begin{align}
a^{m·(n+1)} &= a^{m·n + m} \\\\
&= a^{m·n}·a^m \\\\
&= (a^m)^n·a^m &&\\text{[por HI]} \\\\
&= (a^m)^{n+1} &&\\text{[por pow_succ']}
\\end{align}
<h2>2. Demostraciones con Lean4</h2>
<pre lang="lean">
import Mathlib.Algebra.GroupPower.Basic
open Nat
variable {M : Type} [Monoid M]
variable (a : M)
variable (m n : ℕ)
-- 1ª demostración
-- ===============
example : a^(m * n) = (a^m)^n :=
by
induction' n with n HI
. calc a^(m * 0)
= a^0 := congrArg (a ^ .) (Nat.mul_zero m)
_ = 1 := pow_zero a
_ = (a^m)^0 := (pow_zero (a^m)).symm
. calc a^(m * succ n)
= a^(m * n + m) := congrArg (a ^ .) (Nat.mul_succ m n)
_ = a^(m * n) * a^m := pow_add a (m * n) m
_ = (a^m)^n * a^m := congrArg (. * a^m) HI
_ = (a^m)^(succ n) := (pow_succ' (a^m) n).symm
-- 2ª demostración
-- ===============
example : a^(m * n) = (a^m)^n :=
by
induction' n with n HI
. calc a^(m * 0)
= a^0 := by simp only [Nat.mul_zero]
_ = 1 := by simp only [_root_.pow_zero]
_ = (a^m)^0 := by simp only [_root_.pow_zero]
. calc a^(m * succ n)
= a^(m * n + m) := by simp only [Nat.mul_succ]
_ = a^(m * n) * a^m := by simp only [pow_add]
_ = (a^m)^n * a^m := by simp only [HI]
_ = (a^m)^succ n := by simp only [_root_.pow_succ']
-- 3ª demostración
-- ===============
example : a^(m * n) = (a^m)^n :=
by
induction' n with n HI
. calc a^(m * 0)
= a^0 := by simp [Nat.mul_zero]
_ = 1 := by simp
_ = (a^m)^0 := by simp
. calc a^(m * succ n)
= a^(m * n + m) := by simp [Nat.mul_succ]
_ = a^(m * n) * a^m := by simp [pow_add]
_ = (a^m)^n * a^m := by simp [HI]
_ = (a^m)^succ n := by simp [_root_.pow_succ']
-- 4ª demostración
-- ===============
example : a^(m * n) = (a^m)^n :=
by
induction' n with n HI
. simp [Nat.mul_zero]
. simp [Nat.mul_succ,
pow_add,
HI,
_root_.pow_succ']
-- 5ª demostración
-- ===============
example : a^(m * n) = (a^m)^n :=
by
induction' n with n HI
. -- ⊢ a ^ (m * zero) = (a ^ m) ^ zero
rw [Nat.mul_zero]
-- ⊢ a ^ 0 = (a ^ m) ^ zero
rw [_root_.pow_zero]
-- ⊢ 1 = (a ^ m) ^ zero
rw [_root_.pow_zero]
. -- ⊢ a ^ (m * succ n) = (a ^ m) ^ succ n
rw [Nat.mul_succ]
-- ⊢ a ^ (m * n + m) = (a ^ m) ^ succ n
rw [pow_add]
-- ⊢ a ^ (m * n) * a ^ m = (a ^ m) ^ succ n
rw [HI]
-- ⊢ (a ^ m) ^ n * a ^ m = (a ^ m) ^ succ n
rw [_root_.pow_succ']
-- 6ª demostración
-- ===============
example : a^(m * n) = (a^m)^n :=
by
induction' n with n HI
. rw [Nat.mul_zero, _root_.pow_zero, _root_.pow_zero]
. rw [Nat.mul_succ, pow_add, HI, _root_.pow_succ']
-- 7ª demostración
-- ===============
example : a^(m * n) = (a^m)^n :=
pow_mul a m n
-- Lemas usados
-- ============
-- #check (Nat.mul_succ n m : n * succ m = n * m + n)
-- #check (Nat.mul_zero m : m * 0 = 0)
-- #check (pow_add a m n : a ^ (m + n) = a ^ m * a ^ n)
-- #check (pow_mul a m n : a ^ (m * n) = (a ^ m) ^ n)
-- #check (pow_succ' a n : a ^ (n + 1) = a ^ n * a)
-- #check (pow_zero a : a ^ 0 = 1)
</pre>
Se puede interactuar con las demostraciones anteriores en [Lean 4 Web](https://live.lean-lang.org/#url=https://raw.githubusercontent.com/jaalonso/Calculemus2/main/src/Potencias_de_potencias_en_monoides.lean).
<h2>3. Demostraciones con Isabelle/HOL</h2>
<pre lang="isar">
theory Potencias_de_potencias_en_monoides
imports Main
begin
context monoid_mult
begin
(* 1ª demostración *)
lemma "a^(m * n) = (a^m)^n"
proof (induct n)
have "a ^ (m * 0) = a ^ 0"
by (simp only: mult_0_right)
also have "… = 1"
by (simp only: power_0)
also have "… = (a ^ m) ^ 0"
by (simp only: power_0)
finally show "a ^ (m * 0) = (a ^ m) ^ 0"
by this
next
fix n
assume HI : "a ^ (m * n) = (a ^ m) ^ n"
have "a ^ (m * Suc n) = a ^ (m + m * n)"
by (simp only: mult_Suc_right)
also have "… = a ^ m * a ^ (m * n)"
by (simp only: power_add)
also have "… = a ^ m * (a ^ m) ^ n"
by (simp only: HI)
also have "… = (a ^ m) ^ Suc n"
by (simp only: power_Suc)
finally show "a ^ (m * Suc n) = (a ^ m) ^ Suc n"
by this
qed
(* 2ª demostración *)
lemma "a^(m * n) = (a^m)^n"
proof (induct n)
have "a ^ (m * 0) = a ^ 0" by simp
also have "… = 1" by simp
also have "… = (a ^ m) ^ 0" by simp
finally show "a ^ (m * 0) = (a ^ m) ^ 0" .
next
fix n
assume HI : "a ^ (m * n) = (a ^ m) ^ n"
have "a ^ (m * Suc n) = a ^ (m + m * n)" by simp
also have "… = a ^ m * a ^ (m * n)" by (simp add: power_add)
also have "… = a ^ m * (a ^ m) ^ n" using HI by simp
also have "… = (a ^ m) ^ Suc n" by simp
finally show "a ^ (m * Suc n) =
(a ^ m) ^ Suc n" .
qed
(* 3ª demostración *)
lemma "a^(m * n) = (a^m)^n"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case by (simp add: power_add)
qed
(* 4ª demostración *)
lemma "a^(m * n) = (a^m)^n"
by (induct n) (simp_all add: power_add)
(* 5ª demostración *)
lemma "a^(m * n) = (a^m)^n"
by (simp only: power_mult)
end
end
</pre>