Demostrar con Lean4 que si \(M\) es un monoide, \(a \u2208 M\) y \(m, n \u2208 \u2115\), entonces
\n\[ a^{m\u00b7n} = (a^m)^n \]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Algebra.GroupPower.Basic\nopen Nat\n\nvariable {M : Type} [Monoid M]\nvariable (a : M)\nvariable (m n : \u2115)\n\nexample : a^(m * n) = (a^m)^n :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Por inducci\u00f3n en \(n\).<\/p>\n
Caso base<\/strong>: Supongamos que \(n = 0\). Entonces,
\n\begin{align}
\n a^{m\u00b70} &= a^0 \\
\n &= 1 &&\text{[por pow_zero]} \\
\n &= (a^m)^0 &&\text{[por pow_zero]}
\n\end{align}<\/p>\nPaso de induci\u00f3n: Supogamos que se verifica para \(n\); es decir,
\n\[ a^{m\u00b7n} = (a^m)^n \tag{HI} \]
\nEntonces,
\n\begin{align}
\n a^{m\u00b7(n+1)} &= a^{m\u00b7n + m} \\
\n &= a^{m\u00b7n}\u00b7a^m \\
\n &= (a^m)^n\u00b7a^m &&\text{[por HI]} \\
\n &= (a^m)^{n+1} &&\text{[por pow_succ’]}
\n\end{align}<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Algebra.GroupPower.Basic\nopen Nat\n\nvariable {M : Type} [Monoid M]\nvariable (a : M)\nvariable (m n : \u2115)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a^(m * n) = (a^m)^n :=\nby\n induction' n with n HI\n . calc a^(m * 0)\n = a^0 := congrArg (a ^ .) (Nat.mul_zero m)\n _ = 1 := pow_zero a\n _ = (a^m)^0 := (pow_zero (a^m)).symm\n . calc a^(m * succ n)\n = a^(m * n + m) := congrArg (a ^ .) (Nat.mul_succ m n)\n _ = a^(m * n) * a^m := pow_add a (m * n) m\n _ = (a^m)^n * a^m := congrArg (. * a^m) HI\n _ = (a^m)^(succ n) := (pow_succ' (a^m) n).symm\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a^(m * n) = (a^m)^n :=\nby\n induction' n with n HI\n . calc a^(m * 0)\n = a^0 := by simp only [Nat.mul_zero]\n _ = 1 := by simp only [_root_.pow_zero]\n _ = (a^m)^0 := by simp only [_root_.pow_zero]\n . calc a^(m * succ n)\n = a^(m * n + m) := by simp only [Nat.mul_succ]\n _ = a^(m * n) * a^m := by simp only [pow_add]\n _ = (a^m)^n * a^m := by simp only [HI]\n _ = (a^m)^succ n := by simp only [_root_.pow_succ']\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a^(m * n) = (a^m)^n :=\nby\n induction' n with n HI\n . calc a^(m * 0)\n = a^0 := by simp [Nat.mul_zero]\n _ = 1 := by simp\n _ = (a^m)^0 := by simp\n . calc a^(m * succ n)\n = a^(m * n + m) := by simp [Nat.mul_succ]\n _ = a^(m * n) * a^m := by simp [pow_add]\n _ = (a^m)^n * a^m := by simp [HI]\n _ = (a^m)^succ n := by simp [_root_.pow_succ']\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a^(m * n) = (a^m)^n :=\nby\n induction' n with n HI\n . simp [Nat.mul_zero]\n . simp [Nat.mul_succ,\n pow_add,\n HI,\n _root_.pow_succ']\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a^(m * n) = (a^m)^n :=\nby\n induction' n with n HI\n . -- \u22a2 a ^ (m * zero) = (a ^ m) ^ zero\n rw [Nat.mul_zero]\n -- \u22a2 a ^ 0 = (a ^ m) ^ zero\n rw [_root_.pow_zero]\n -- \u22a2 1 = (a ^ m) ^ zero\n rw [_root_.pow_zero]\n . -- \u22a2 a ^ (m * succ n) = (a ^ m) ^ succ n\n rw [Nat.mul_succ]\n -- \u22a2 a ^ (m * n + m) = (a ^ m) ^ succ n\n rw [pow_add]\n -- \u22a2 a ^ (m * n) * a ^ m = (a ^ m) ^ succ n\n rw [HI]\n -- \u22a2 (a ^ m) ^ n * a ^ m = (a ^ m) ^ succ n\n rw [_root_.pow_succ']\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a^(m * n) = (a^m)^n :=\nby\n induction' n with n HI\n . rw [Nat.mul_zero, _root_.pow_zero, _root_.pow_zero]\n . rw [Nat.mul_succ, pow_add, HI, _root_.pow_succ']\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample : a^(m * n) = (a^m)^n :=\npow_mul a m n\n\n-- Lemas usados\n-- ============\n\n-- #check (Nat.mul_succ n m : n * succ m = n * m + n)\n-- #check (Nat.mul_zero m : m * 0 = 0)\n-- #check (pow_add a m n : a ^ (m + n) = a ^ m * a ^ n)\n-- #check (pow_mul a m n : a ^ (m * n) = (a ^ m) ^ n)\n-- #check (pow_succ' a n : a ^ (n + 1) = a ^ n * a)\n-- #check (pow_zero a : a ^ 0 = 1)\n<\/pre>\n