La semana en Calculemus (18 de mayo de 2024)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. Si G es un grupo y a, b ∈ G tales que ab = 1 entonces a⁻¹ = b
- 2. Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹
- 3. Si G un grupo y a ∈ G, entonces (a⁻¹)⁻¹ = a
- 4. Si G es un grupo y a, b, c ∈ G tales que a·b = a·c, entonces b = c
- 5. Si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces a^(m·n) = (a^m)^n
A continuación se muestran las soluciones.
1. Si G es un grupo y a, b ∈ G tales que ab = 1 entonces a⁻¹ = b
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
1.1. Demostración en lenguaje natural
Por la siguiente cadena de igualdades \begin{align} a⁻¹ &= a⁻¹·1 &&\text{[porque 1 es neutro]} \newline &= a⁻¹·(a·b) &&\text{[por hipótesis]} \newline &= (a⁻¹·a)·b &&\text{[por la asociativa]} \newline &= 1·b &&\text{[porque a⁻¹ es el inverso de a]} \newline &= b &&\text{[porque 1 es neutro]} \end{align}
1.2. Demostraciones con Lean4
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] variable {a b : G} -- 1ª demostración -- =============== example (h : a * b = 1) : a⁻¹ = b := calc a⁻¹ = a⁻¹ * 1 := (mul_one a⁻¹).symm _ = a⁻¹ * (a * b) := congrArg (a⁻¹ * .) h.symm _ = (a⁻¹ * a) * b := (mul_assoc a⁻¹ a b).symm _ = 1 * b := congrArg (. * b) (inv_mul_self a) _ = b := one_mul b -- 2ª demostración -- =============== example (h : a * b = 1) : a⁻¹ = b := calc a⁻¹ = a⁻¹ * 1 := by simp only [mul_one] _ = a⁻¹ * (a * b) := by simp only [h] _ = (a⁻¹ * a) * b := by simp only [mul_assoc] _ = 1 * b := by simp only [inv_mul_self] _ = b := by simp only [one_mul] -- 3ª demostración -- =============== example (h : a * b = 1) : a⁻¹ = b := calc a⁻¹ = a⁻¹ * 1 := by simp _ = a⁻¹ * (a * b) := by simp [h] _ = (a⁻¹ * a) * b := by simp _ = 1 * b := by simp _ = b := by simp -- 4ª demostración -- =============== example (h : a * b = 1) : a⁻¹ = b := calc a⁻¹ = a⁻¹ * (a * b) := by simp [h] _ = b := by simp -- 5ª demostración -- =============== example (h : b * a = 1) : b = a⁻¹ := eq_inv_iff_mul_eq_one.mpr h -- Lemas usados -- ============ -- variable (c : G) -- #check (eq_inv_iff_mul_eq_one : a = b⁻¹ ↔ a * b = 1) -- #check (inv_mul_self a : a⁻¹ * a = 1) -- #check (mul_assoc a b c : (a * b) * c = a * (b * c)) -- #check (mul_one a : a * 1 = a) -- #check (one_mul a : 1 * a = a)
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
1.3. Demostraciones con Isabelle/HOL
theory Unicidad_de_los_inversos_en_los_grupos imports Main begin context group begin (* 1ª demostración *) lemma assumes "a * b = 1" shows "inverse a = b" proof - have "inverse a = inverse a * 1" by (simp only: right_neutral) also have "… = inverse a * (a * b)" by (simp only: assms(1)) also have "… = (inverse a * a) * b" by (simp only: assoc [symmetric]) also have "… = 1 * b" by (simp only: left_inverse) also have "… = b" by (simp only: left_neutral) finally show "inverse a = b" by this qed (* 2ª demostración *) lemma assumes "a * b = 1" shows "inverse a = b" proof - have "inverse a = inverse a * 1" by simp also have "… = inverse a * (a * b)" using assms by simp also have "… = (inverse a * a) * b" by (simp add: assoc [symmetric]) also have "… = 1 * b" by simp also have "… = b" by simp finally show "inverse a = b" . qed (* 3ª demostración *) lemma assumes "a * b = 1" shows "inverse a = b" proof - from assms have "inverse a * (a * b) = inverse a" by simp then show "inverse a = b" by (simp add: assoc [symmetric]) qed (* 4ª demostración *) lemma assumes "a * b = 1" shows "inverse a = b" using assms by (simp only: inverse_unique) end end
2. Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹
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
2.1. Demostración en lenguaje natural
Teniendo en cuenta la propiedad \[(∀ a, b ∈ G)[ab = 1 → a⁻¹ = b] \] basta demostrar que \[(a·b)·(b⁻¹·a⁻¹) = 1.\] que se demuestra mediante la siguiente cadena de igualdades \begin{align} (a·b)·(b⁻¹·a⁻¹) &= a·(b·(b⁻¹·a⁻¹)) &&\text{[por la asociativa]} \newline &= a·((b·b⁻¹)·a⁻¹) &&\text{[por la asociativa]} \newline &= a·(1·a⁻¹) &&\text{[por producto con inverso]} \newline &= a·a⁻¹ &&\text{[por producto con uno]} \newline &= 1 &&\text{[por producto con inverso]} \end{align}
2.2. Demostraciones con Lean4
import Mathlib.Algebra.Group.Defs variable {G : Type _} [Group G] variable (a b : G) lemma aux : (a * b) * (b⁻¹ * a⁻¹) = 1 := calc (a * b) * (b⁻¹ * a⁻¹) = a * (b * (b⁻¹ * a⁻¹)) := by rw [mul_assoc] _ = a * ((b * b⁻¹) * a⁻¹) := by rw [mul_assoc] _ = a * (1 * a⁻¹) := by rw [mul_right_inv] _ = a * a⁻¹ := by rw [one_mul] _ = 1 := by rw [mul_right_inv] -- 1ª demostración example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by have h1 : (a * b) * (b⁻¹ * a⁻¹) = 1 := aux a b show (a * b)⁻¹ = b⁻¹ * a⁻¹ exact inv_eq_of_mul_eq_one_right h1 -- 3ª demostración example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by have h1 : (a * b) * (b⁻¹ * a⁻¹) = 1 := aux a b show (a * b)⁻¹ = b⁻¹ * a⁻¹ simp [h1] -- 4ª demostración example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by have h1 : (a * b) * (b⁻¹ * a⁻¹) = 1 := aux a b simp [h1] -- 5ª demostración example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by apply inv_eq_of_mul_eq_one_right rw [aux] -- 6ª demostración example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by exact mul_inv_rev a b -- 7ª demostración example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by simp
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
2.3. Demostraciones con Isabelle/HOL
theory Inverso_del_producto imports Main begin context group begin (* 1ª demostración *) lemma "inverse (a * b) = inverse b * inverse a" proof (rule inverse_unique) have "(a * b) * (inverse b * inverse a) = ((a * b) * inverse b) * inverse a" by (simp only: assoc) also have "… = (a * (b * inverse b)) * inverse a" by (simp only: assoc) also have "… = (a * 1) * inverse a" by (simp only: right_inverse) also have "… = a * inverse a" by (simp only: right_neutral) also have "… = 1" by (simp only: right_inverse) finally show "a * b * (inverse b * inverse a) = 1" by this qed (* 2ª demostración *) lemma "inverse (a * b) = inverse b * inverse a" proof (rule inverse_unique) have "(a * b) * (inverse b * inverse a) = ((a * b) * inverse b) * inverse a" by (simp only: assoc) also have "… = (a * (b * inverse b)) * inverse a" by (simp only: assoc) also have "… = (a * 1) * inverse a" by simp also have "… = a * inverse a" by simp also have "… = 1" by simp finally show "a * b * (inverse b * inverse a) = 1" . qed (* 3ª demostración *) lemma "inverse (a * b) = inverse b * inverse a" proof (rule inverse_unique) have "a * b * (inverse b * inverse a) = a * (b * inverse b) * inverse a" by (simp only: assoc) also have "… = 1" by simp finally show "a * b * (inverse b * inverse a) = 1" . qed (* 4ª demostración *) lemma "inverse (a * b) = inverse b * inverse a" by (simp only: inverse_distrib_swap) end end
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 12.
3. Si G un grupo y a ∈ G, entonces (a⁻¹)⁻¹ = a
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
3.1. Demostración en lenguaje natural
Por la siguiente cadena de igualdades \begin{align} (a⁻¹)⁻¹ &= (a⁻¹)⁻¹·1 &&\text{[porque \(1\) es neutro]} \newline &= (a⁻¹)⁻¹·(a⁻¹·a) &&\text{[porque \(a⁻¹\) es el inverso de \(a\)]} \newline &= ((a⁻¹)⁻¹·a⁻¹)·a &&\text{[por la asociativa]} \newline &= 1·a &&\text{[porque \((a⁻¹)⁻¹\) es el inverso de \(a⁻¹\)]} \newline &= a &&\text{[porque \(1\) es neutro]} \end{align}
3.2. Demostraciones con Lean4
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] variable {a : G} -- 1ª demostración -- =============== example : (a⁻¹)⁻¹ = a := calc (a⁻¹)⁻¹ = (a⁻¹)⁻¹ * 1 := (mul_one (a⁻¹)⁻¹).symm _ = (a⁻¹)⁻¹ * (a⁻¹ * a) := congrArg ((a⁻¹)⁻¹ * .) (inv_mul_self a).symm _ = ((a⁻¹)⁻¹ * a⁻¹) * a := (mul_assoc _ _ _).symm _ = 1 * a := congrArg (. * a) (inv_mul_self a⁻¹) _ = a := one_mul a -- 2ª demostración -- =============== example : (a⁻¹)⁻¹ = a := calc (a⁻¹)⁻¹ = (a⁻¹)⁻¹ * 1 := by simp only [mul_one] _ = (a⁻¹)⁻¹ * (a⁻¹ * a) := by simp only [inv_mul_self] _ = ((a⁻¹)⁻¹ * a⁻¹) * a := by simp only [mul_assoc] _ = 1 * a := by simp only [inv_mul_self] _ = a := by simp only [one_mul] -- 3ª demostración -- =============== example : (a⁻¹)⁻¹ = a := calc (a⁻¹)⁻¹ = (a⁻¹)⁻¹ * 1 := by simp _ = (a⁻¹)⁻¹ * (a⁻¹ * a) := by simp _ = ((a⁻¹)⁻¹ * a⁻¹) * a := by simp _ = 1 * a := by simp _ = a := by simp -- 4ª demostración -- =============== example : (a⁻¹)⁻¹ = a := by apply mul_eq_one_iff_inv_eq.mp -- ⊢ a⁻¹ * a = 1 exact mul_left_inv a -- 5ª demostración -- =============== example : (a⁻¹)⁻¹ = a := mul_eq_one_iff_inv_eq.mp (mul_left_inv a) -- 6ª demostración -- =============== example : (a⁻¹)⁻¹ = a:= inv_inv a -- 7ª demostración -- =============== example : (a⁻¹)⁻¹ = a:= by simp -- Lemas usados -- ============ -- variable (b c : G) -- #check (inv_inv a : (a⁻¹)⁻¹ = a) -- #check (inv_mul_self a : a⁻¹ * a = 1) -- #check (mul_assoc a b c : (a * b) * c = a * (b * c)) -- #check (mul_eq_one_iff_inv_eq : a * b = 1 ↔ a⁻¹ = b) -- #check (mul_left_inv a : a⁻¹ * a = 1) -- #check (mul_one a : a * 1 = a) -- #check (one_mul a : 1 * a = a)
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3.3. Demostraciones con Isabelle/HOL
theory Inverso_del_inverso_en_grupos imports Main begin context group begin (* 1ª demostración *) lemma "inverse (inverse a) = a" proof - have "inverse (inverse a) = (inverse (inverse a)) * 1" by (simp only: right_neutral) also have "… = inverse (inverse a) * (inverse a * a)" by (simp only: left_inverse) also have "… = (inverse (inverse a) * inverse a) * a" by (simp only: assoc) also have "… = 1 * a" by (simp only: left_inverse) also have "… = a" by (simp only: left_neutral) finally show "inverse (inverse a) = a" by this qed (* 2ª demostración *) lemma "inverse (inverse a) = a" proof - have "inverse (inverse a) = (inverse (inverse a)) * 1" by simp also have "… = inverse (inverse a) * (inverse a * a)" by simp also have "… = (inverse (inverse a) * inverse a) * a" by simp also have "… = 1 * a" by simp finally show "inverse (inverse a) = a" by simp qed (* 3ª demostración *) lemma "inverse (inverse a) = a" proof (rule inverse_unique) show "inverse a * a = 1" by (simp only: left_inverse) qed (* 4ª demostración *) lemma "inverse (inverse a) = a" proof (rule inverse_unique) show "inverse a * a = 1" by simp qed (* 5ª demostración *) lemma "inverse (inverse a) = a" by (rule inverse_unique) simp (* 6ª demostración *) lemma "inverse (inverse a) = a" by (simp only: inverse_inverse) (* 7ª demostración *) lemma "inverse (inverse a) = a" by simp end end
4. 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\) 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
4.1. Demostración en lenguaje natural
Por la siguiente cadena de igualdades \begin{align} b &= 1·b &&\text{[porque \(1\) es neutro]} \newline &= (a⁻¹·a)·b &&\text{[porque \(a⁻¹\) es el inverso de \(a\)]} \newline &= a⁻¹·(a·b) &&\text{[por la asociativa]} \newline &= a⁻¹·(a·c) &&\text{[por la hipótesis]} \newline &= (a⁻¹·a)·c &&\text{[por la asociativa]} \newline &= 1·c &&\text{[porque \(a⁻¹\) es el inverso de \(a\)]} \newline &= c &&\text{[porque 1 es neutro]} \end{align}
4.2. Demostraciones con Lean4
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] variable {a b c : G} -- 1ª demostración -- =============== example (h: a * b = a * c) : b = c := calc b = 1 * b := (one_mul b).symm _ = (a⁻¹ * a) * b := congrArg (. * b) (inv_mul_self a).symm _ = a⁻¹ * (a * b) := mul_assoc a⁻¹ a b _ = a⁻¹ * (a * c) := congrArg (a⁻¹ * .) h _ = (a⁻¹ * a) * c := (mul_assoc a⁻¹ a c).symm _ = 1 * c := congrArg (. * c) (inv_mul_self a) _ = c := one_mul c -- 2ª demostración -- =============== example (h: a * b = a * c) : b = c := calc b = 1 * b := by rw [one_mul] _ = (a⁻¹ * a) * b := by rw [inv_mul_self] _ = a⁻¹ * (a * b) := by rw [mul_assoc] _ = a⁻¹ * (a * c) := by rw [h] _ = (a⁻¹ * a) * c := by rw [mul_assoc] _ = 1 * c := by rw [inv_mul_self] _ = c := by rw [one_mul] -- 3ª demostración -- =============== example (h: a * b = a * c) : b = c := calc b = 1 * b := by simp _ = (a⁻¹ * a) * b := by simp _ = a⁻¹ * (a * b) := by simp _ = a⁻¹ * (a * c) := by simp [h] _ = (a⁻¹ * a) * c := by simp _ = 1 * c := by simp _ = c := by simp -- 4ª demostración -- =============== example (h: a * b = a * c) : b = c := calc b = a⁻¹ * (a * b) := by simp _ = a⁻¹ * (a * c) := by simp [h] _ = c := by simp -- 4ª demostración -- =============== example (h: a * b = a * c) : b = c := mul_left_cancel h -- 5ª demostración -- =============== example (h: a * b = a * c) : b = c := by aesop -- Lemas usados -- ============ -- #check (inv_mul_self a : a⁻¹ * a = 1) -- #check (mul_assoc a b c : (a * b) * c = a * (b * c)) -- #check (mul_left_cancel : a * b = a * c → b = c) -- #check (one_mul a : 1 * a = a)
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
4.3. Demostraciones con Isabelle/HOL
theory Propiedad_cancelativa_en_grupos imports Main begin context group begin (* 1ª demostración *) lemma assumes "a * b = a * c" shows "b = c" proof - have "b = 1 * b" by (simp only: left_neutral) also have "… = (inverse a * a) * b" by (simp only: left_inverse) also have "… = inverse a * (a * b)" by (simp only: assoc) also have "… = inverse a * (a * c)" by (simp only: ‹a * b = a * c›) also have "… = (inverse a * a) * c" by (simp only: assoc) also have "… = 1 * c" by (simp only: left_inverse) also have "… = c" by (simp only: left_neutral) finally show "b = c" by this qed (* 2ª demostración *) lemma assumes "a * b = a * c" shows "b = c" proof - have "b = 1 * b" by simp also have "… = (inverse a * a) * b" by simp also have "… = inverse a * (a * b)" by (simp only: assoc) also have "… = inverse a * (a * c)" using ‹a * b = a * c› by simp also have "… = (inverse a * a) * c" by (simp only: assoc) also have "… = 1 * c" by simp finally show "b = c" by simp qed (* 3ª demostración *) lemma assumes "a * b = a * c" shows "b = c" proof - have "b = (inverse a * a) * b" by simp also have "… = inverse a * (a * b)" by (simp only: assoc) also have "… = inverse a * (a * c)" using ‹a * b = a * c› by simp also have "… = (inverse a * a) * c" by (simp only: assoc) finally show "b = c" by simp qed (* 4ª demostración *) lemma assumes "a * b = a * c" shows "b = c" proof - have "inverse a * (a * b) = inverse a * (a * c)" by (simp only: ‹a * b = a * c›) then have "(inverse a * a) * b = (inverse a * a) * c" by (simp only: assoc) then have "1 * b = 1 * c" by (simp only: left_inverse) then show "b = c" by (simp only: left_neutral) qed (* 5ª demostración *) lemma assumes "a * b = a * c" shows "b = c" proof - have "inverse a * (a * b) = inverse a * (a * c)" by (simp only: ‹a * b = a * c›) then have "(inverse a * a) * b = (inverse a * a) * c" by (simp only: assoc) then have "1 * b = 1 * c" by (simp only: left_inverse) then show "b = c" by (simp only: left_neutral) qed (* 6ª demostración *) lemma assumes "a * b = a * c" shows "b = c" proof - have "inverse a * (a * b) = inverse a * (a * c)" using ‹a * b = a * c› by simp then have "(inverse a * a) * b = (inverse a * a) * c" by (simp only: assoc) then have "1 * b = 1 * c" by simp then show "b = c" by simp qed (* 7ª demostración *) lemma assumes "a * b = a * c" shows "b = c" using assms by (simp only: left_cancel) end end
5. Si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces a^(m·n) = (a^m)^n
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
5.1. Demostración en lenguaje natural
Por inducción en \(n\).
Caso base: Supongamos que \(n = 0\). Entonces, \begin{align} a^{m·0} &= a^0 \newline &= 1 &&\text{[por pow_zero]} \newline &= (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} \newline &= a^{m·n}·a^m \newline &= (a^m)^n·a^m &&\text{[por HI]} \newline &= (a^m)^{n+1} &&\text{[por pow_succ']} \end{align}
5.2. Demostraciones con Lean4
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)
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
5.3. Demostraciones con Isabelle/HOL
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