La semana en Calculemus (11 de mayo de 2024)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. Producto de potencias de la misma base en monoides
- 2. Equivalencia de inversos iguales al neutro
- 3. Unicidad de inversos en monoides
- 4. Caracterización de producto igual al primer factor
- 5. Unicidad del elemento neutro en los grupos
A continuación se muestran las soluciones.
1. 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 |
1. Demostración en lenguaje natural
Por inducción en \(m\).
Base:
\begin{align}
x^{0 + n} &= x^n \\
&= 1 · x^n \\
&= x^0 · x^n &&\text{[por pow_zero]}
\end{align}
Paso: Supongamos que
\[ x^{m + n} = x^m x^n \tag{HI} \]
Entonces
\begin{align}
x^{(m+1) + n} &= x^{(m + n) + 1} \\
&= x · x^{m + n} &&\text{[por pow_succ]} \\
&= x · (x^m · x^n) &&\text{[por HI]} \\
&= (x · x^m) · x^n \\
&= x^{m+1} · x^n &&\text{[por pow_succ]}
\end{align}
2. Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 |
import Mathlib.Algebra.Group.Defs import Mathlib.Algebra.GroupPower.Basic open Nat variable {M : Type} [Monoid M] variable (x : M) variable (m n : ℕ) -- 1ª demostración -- =============== example : x^(m + n) = x^m * x^n := by induction' m with m HI . calc x^(0 + n) = x^n := congrArg (x ^ .) (Nat.zero_add n) _ = 1 * x^n := (Monoid.one_mul (x^n)).symm _ = x^0 * x^n := congrArg (. * (x^n)) (pow_zero x).symm . calc x^(succ m + n) = x^succ (m + n) := congrArg (x ^.) (succ_add m n) _ = x * x^(m + n) := pow_succ x (m + n) _ = x * (x^m * x^n) := congrArg (x * .) HI _ = (x * x^m) * x^n := (mul_assoc x (x^m) (x^n)).symm _ = x^succ m * x^n := congrArg (. * x^n) (pow_succ x m).symm -- 2ª demostración -- =============== example : x^(m + n) = x^m * x^n := by induction' m with m HI . calc x^(0 + n) = x^n := by simp only [Nat.zero_add] _ = 1 * x^n := by simp only [Monoid.one_mul] _ = x^0 * x^n := by simp only [_root_.pow_zero] . calc x^(succ m + n) = x^succ (m + n) := by simp only [succ_add] _ = x * x^(m + n) := by simp only [_root_.pow_succ] _ = x * (x^m * x^n) := by simp only [HI] _ = (x * x^m) * x^n := (mul_assoc x (x^m) (x^n)).symm _ = x^succ m * x^n := by simp only [_root_.pow_succ] -- 3ª demostración -- =============== example : x^(m + n) = x^m * x^n := by induction' m with m HI . calc x^(0 + n) = x^n := by simp [Nat.zero_add] _ = 1 * x^n := by simp _ = x^0 * x^n := by simp . calc x^(succ m + n) = x^succ (m + n) := by simp [succ_add] _ = x * x^(m + n) := by simp [_root_.pow_succ] _ = x * (x^m * x^n) := by simp [HI] _ = (x * x^m) * x^n := (mul_assoc x (x^m) (x^n)).symm _ = x^succ m * x^n := by simp [_root_.pow_succ] -- 4ª demostración -- =============== example : x^(m + n) = x^m * x^n := pow_add x m n -- Lemas usados -- ============ -- variable (y z : M) -- #check (Monoid.one_mul x : 1 * x = x) -- #check (Nat.zero_add n : 0 + n = n) -- #check (mul_assoc x y z : (x * y) * z = x * (y * z)) -- #check (pow_add x m n : x^(m + n) = x^m * x^n) -- #check (pow_succ x n : x ^ succ n = x * x ^ n) -- #check (pow_zero x : x ^ 0 = 1) -- #check (succ_add n m : succ n + m = succ (n + m)) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones con Isabelle/HOL
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 |
theory Producto_de_potencias_de_la_misma_base_en_monoides imports Main begin context monoid_mult begin (* 1ª demostración *) lemma "x ^ (m + n) = x ^ m * x ^ n" proof (induct m) have "x ^ (0 + n) = x ^ n" by (simp only: add_0) also have "… = 1 * x ^ n" by (simp only: mult_1_left) also have "… = x ^ 0 * x ^ n" by (simp only: power_0) finally show "x ^ (0 + n) = x ^ 0 * x ^ n" by this next fix m assume HI : "x ^ (m + n) = x ^ m * x ^ n" have "x ^ (Suc m + n) = x ^ Suc (m + n)" by (simp only: add_Suc) also have "… = x * x ^ (m + n)" by (simp only: power_Suc) also have "… = x * (x ^ m * x ^ n)" by (simp only: HI) also have "… = (x * x ^ m) * x ^ n" by (simp only: mult_assoc) also have "… = x ^ Suc m * x ^ n" by (simp only: power_Suc) finally show "x ^ (Suc m + n) = x ^ Suc m * x ^ n" by this qed (* 2ª demostración *) lemma "x ^ (m + n) = x ^ m * x ^ n" proof (induct m) have "x ^ (0 + n) = x ^ n" by simp also have "… = 1 * x ^ n" by simp also have "… = x ^ 0 * x ^ n" by simp finally show "x ^ (0 + n) = x ^ 0 * x ^ n" by this next fix m assume HI : "x ^ (m + n) = x ^ m * x ^ n" have "x ^ (Suc m + n) = x ^ Suc (m + n)" by simp also have "… = x * x ^ (m + n)" by simp also have "… = x * (x ^ m * x ^ n)" using HI by simp also have "… = (x * x ^ m) * x ^ n" by (simp add: mult_assoc) also have "… = x ^ Suc m * x ^ n" by simp finally show "x ^ (Suc m + n) = x ^ Suc m * x ^ n" by this qed (* 3ª demostración *) lemma "x ^ (m + n) = x ^ m * x ^ n" proof (induct m) case 0 then show ?case by simp next case (Suc m) then show ?case by (simp add: algebra_simps) qed (* 4ª demostración *) lemma "x ^ (m + n) = x ^ m * x ^ n" by (induct m) (simp_all add: algebra_simps) (* 5ª demostración *) lemma "x ^ (m + n) = x ^ m * x ^ n" by (simp only: power_add) end end |
2. Equivalencia de inversos iguales al neutro
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:
|
1 2 3 4 5 6 7 8 9 |
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 |
1. Demostración en lenguaje natural
Demostraremos las dos implicaciones.
(⟹) Supongamos que \(a = 1\). Entonces,
\begin{align}
b &= 1·b &&\text{[por neutro por la izquierda]} \\
&= a·b &&\text{[por supuesto]} \\
&= 1 &&\text{[por hipótesis]}
\end{align}
(⟸) Supongamos que \(b = 1\). Entonces,
\begin{align}
a &= a·1 &&\text{[por neutro por la derecha]} \\
&= a·b &&\text{[por supuesto]} \\
&= 1 &&\text{[por hipótesis]}
\end{align}
2. Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 |
import Mathlib.Algebra.Group.Basic variable {M : Type} [Monoid M] variable {a b : M} -- 1ª demostración -- =============== example (h : a * b = 1) : a = 1 ↔ b = 1 := by constructor . -- ⊢ a = 1 → b = 1 intro a1 -- a1 : a = 1 -- ⊢ b = 1 calc b = 1 * b := (one_mul b).symm _ = a * b := congrArg (. * b) a1.symm _ = 1 := h . -- ⊢ b = 1 → a = 1 intro b1 -- b1 : b = 1 -- ⊢ a = 1 calc a = a * 1 := (mul_one a).symm _ = a * b := congrArg (a * .) b1.symm _ = 1 := h -- 2ª demostración -- =============== example (h : a * b = 1) : a = 1 ↔ b = 1 := by constructor . -- ⊢ a = 1 → b = 1 intro a1 -- a1 : a = 1 -- ⊢ b = 1 rw [a1] at h -- h : 1 * b = 1 rw [one_mul] at h -- h : b = 1 exact h . -- ⊢ b = 1 → a = 1 intro b1 -- b1 : b = 1 -- ⊢ a = 1 rw [b1] at h -- h : a * 1 = 1 rw [mul_one] at h -- h : a = 1 exact h -- 3ª demostración -- =============== example (h : a * b = 1) : a = 1 ↔ b = 1 := by constructor . -- ⊢ a = 1 → b = 1 rintro rfl -- h : 1 * b = 1 simpa using h . -- ⊢ b = 1 → a = 1 rintro rfl -- h : a * 1 = 1 simpa using h -- 4ª demostración -- =============== example (h : a * b = 1) : a = 1 ↔ b = 1 := by constructor <;> (rintro rfl; simpa using h) -- 5ª demostración -- =============== example (h : a * b = 1) : a = 1 ↔ b = 1 := eq_one_iff_eq_one_of_mul_eq_one h -- Lemas usados -- ============ -- #check (eq_one_iff_eq_one_of_mul_eq_one : a * b = 1 → (a = 1 ↔ b = 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. Demostraciones con Isabelle/HOL
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 |
theory Equivalencia_de_inversos_iguales_al_neutro imports Main begin context monoid begin (* 1ª demostración *) lemma assumes "a * b = 1" shows "a = 1 ⟷ b = 1" proof (rule iffI) assume "a = 1" have "b = 1 * b" by (simp only: left_neutral) also have "… = a * b" by (simp only: ‹a = 1›) also have "… = 1" by (simp only: ‹a * b = 1›) finally show "b = 1" by this next assume "b = 1" have "a = a * 1" by (simp only: right_neutral) also have "… = a * b" by (simp only: ‹b = 1›) also have "… = 1" by (simp only: ‹a * b = 1›) finally show "a = 1" by this qed (* 2ª demostración *) lemma assumes "a * b = 1" shows "a = 1 ⟷ b = 1" proof assume "a = 1" have "b = 1 * b" by simp also have "… = a * b" using ‹a = 1› by simp also have "… = 1" using ‹a * b = 1› by simp finally show "b = 1" . next assume "b = 1" have "a = a * 1" by simp also have "… = a * b" using ‹b = 1› by simp also have "… = 1" using ‹a * b = 1› by simp finally show "a = 1" . qed (* 3ª demostración *) lemma assumes "a * b = 1" shows "a = 1 ⟷ b = 1" by (metis assms left_neutral right_neutral) end end |
3. Unicidad de inversos en monoides
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:
|
1 2 3 4 5 6 7 8 9 10 |
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 |
1. Demostración en lenguaje natural
Por la siguiente cadena de igualdades
\begin{align}
y &= 1·y &&\text{[por neutro a la izquierda]} \\
&= (x·z)·y &&\text{[por hipótesis]} \\
&= (z·x)·y &&\text{[por la conmutativa]} \\
&= z·(x·y) &&\text{[por la asociativa]} \\
&= z·1 &&\text{[por hipótesis]} \\
&= z &&\text{[por neutro a la derecha]}
\end{align}
2. Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 |
import Mathlib.Algebra.Group.Basic variable {M : Type} [CommMonoid M] variable {x y z : M} -- 1ª demostración -- =============== example (hy : x * y = 1) (hz : x * z = 1) : y = z := calc y = 1 * y := (one_mul y).symm _ = (x * z) * y := congrArg (. * y) hz.symm _ = (z * x) * y := congrArg (. * y) (mul_comm x z) _ = z * (x * y) := mul_assoc z x y _ = z * 1 := congrArg (z * .) hy _ = z := mul_one z -- 2ª demostración -- =============== example (hy : x * y = 1) (hz : x * z = 1) : y = z := calc y = 1 * y := by simp only [one_mul] _ = (x * z) * y := by simp only [hz] _ = (z * x) * y := by simp only [mul_comm] _ = z * (x * y) := by simp only [mul_assoc] _ = z * 1 := by simp only [hy] _ = z := by simp only [mul_one] -- 3ª demostración -- =============== example (hy : x * y = 1) (hz : x * z = 1) : y = z := calc y = 1 * y := by simp _ = (x * z) * y := by simp [hz] _ = (z * x) * y := by simp [mul_comm] _ = z * (x * y) := by simp [mul_assoc] _ = z * 1 := by simp [hy] _ = z := by simp -- 4ª demostración -- =============== example (hy : x * y = 1) (hz : x * z = 1) : y = z := by apply left_inv_eq_right_inv _ hz -- ⊢ y * x = 1 rw [mul_comm] -- ⊢ x * y = 1 exact hy -- 5ª demostración -- =============== example (hy : x * y = 1) (hz : x * z = 1) : y = z := inv_unique hy hz -- Lemas usados -- ============ -- #check (inv_unique : x * y = 1 → x * z = 1 → y = z) -- #check (left_inv_eq_right_inv : y * x = 1 → x * z = 1 → y = z) -- #check (mul_assoc x y z : (x * y) * z = x * (y * z)) -- #check (mul_comm x y : x * y = y * x) -- #check (mul_one x : x * 1 = x) -- #check (one_mul x : 1 * x = x) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones con Isabelle/HOL
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 |
theory Unicidad_de_inversos_en_monoides imports Main begin context comm_monoid begin (* 1ª demostración *) lemma assumes "x * y = 1" "x * z = 1" shows "y = z" proof - have "y = 1 * y" by (simp only: left_neutral) also have "… = (x * z) * y" by (simp only: ‹x * z = 1›) also have "… = (z * x) * y" by (simp only: commute) also have "… = z * (x * y)" by (simp only: assoc) also have "… = z * 1" by (simp only: ‹x * y = 1›) also have "… = z" by (simp only: right_neutral) finally show "y = z" by this qed (* 2ª demostración *) lemma assumes "x * y = 1" "x * z = 1" shows "y = z" proof - have "y = 1 * y" by simp also have "… = (x * z) * y" using assms(2) by simp also have "… = (z * x) * y" by simp also have "… = z * (x * y)" by simp also have "… = z * 1" using assms(1) by simp also have "… = z" by simp finally show "y = z" by this qed (* 3ª demostración *) lemma assumes "x * y = 1" "x * z = 1" shows "y = z" using assms by auto end end |
4. Caracterización de producto igual al primer factor
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
|
1 |
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:
|
1 2 3 4 5 6 7 |
import Mathlib.Algebra.Group.Basic variable {M : Type} [LeftCancelMonoid M] variable {a b : M} example : a * b = a ↔ b = 1 := by sorry |
1. Demostración en lenguaje natural
Demostraremos las dos implicaciones.
(⟹) Supongamos que
\[ a·b = a \]
Por la propiedad del neutro por la derecha tenemos
\[ a·1 = a \]
Por tanto,
\[ a·b = a·1 \]
y, por la propiedad cancelativa,
\[ b = 1 \]
(⟸) Supongamos que \(b = 1\). Entonces,
\begin{align}
a·b &= a·1 \\
&= a &&\text{[por el neutro por la derecha]}
\end{align}
2. Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 |
import Mathlib.Algebra.Group.Basic variable {M : Type} [LeftCancelMonoid M] variable {a b : M} -- 1ª demostración -- =============== example : a * b = a ↔ b = 1 := by constructor . -- ⊢ a * b = a → b = 1 intro h -- h : a * b = a -- ⊢ b = 1 have h1 : a * b = a * 1 := by calc a * b = a := by exact h _ = a * 1 := (mul_one a).symm exact mul_left_cancel h1 . -- ⊢ b = 1 → a * b = a intro h -- h : b = 1 -- ⊢ a * b = a rw [h] -- ⊢ a * 1 = a exact mul_one a -- 2ª demostración -- =============== example : a * b = a ↔ b = 1 := calc a * b = a ↔ a * b = a * 1 := by rw [mul_one] _ ↔ b = 1 := mul_left_cancel_iff -- 3ª demostración -- =============== example : a * b = a ↔ b = 1 := mul_right_eq_self -- 4ª demostración -- =============== example : a * b = a ↔ b = 1 := by aesop -- Lemas usados -- ============ -- variable (c : M) -- #check (mul_left_cancel : a * b = a * c → b = c) -- #check (mul_one a : a * 1 = a) -- #check (mul_right_eq_self : a * b = a ↔ b = 1) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones con Isabelle/HOL
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 |
theory Caracterizacion_de_producto_igual_al_primer_factor imports Main begin context cancel_comm_monoid_add begin (* 1ª demostración *) lemma "a + b = a ⟷ b = 0" proof (rule iffI) assume "a + b = a" then have "a + b = a + 0" by (simp only: add_0_right) then show "b = 0" by (simp only: add_left_cancel) next assume "b = 0" have "a + 0 = a" by (simp only: add_0_right) with ‹b = 0› show "a + b = a" by (rule ssubst) qed (* 2ª demostración *) lemma "a + b = a ⟷ b = 0" proof assume "a + b = a" then have "a + b = a + 0" by simp then show "b = 0" by simp next assume "b = 0" have "a + 0 = a" by simp then show "a + b = a" using ‹b = 0› by simp qed (* 3ª demostración *) lemma "a + b = a ⟷ b = 0" proof - have "(a + b = a) ⟷ (a + b = a + 0)" by (simp only: add_0_right) also have "… ⟷ (b = 0)" by (simp only: add_left_cancel) finally show "a + b = a ⟷ b = 0" by this qed (* 4ª demostración *) lemma "a + b = a ⟷ b = 0" proof - have "(a + b = a) ⟷ (a + b = a + 0)" by simp also have "… ⟷ (b = 0)" by simp finally show "a + b = a ⟷ b = 0" . qed (* 5ª demostración *) lemma "a + b = a ⟷ b = 0" by (simp only: add_cancel_left_right) (* 6ª demostración *) lemma "a + b = a ⟷ b = 0" by auto end end |
5. Unicidad del elemento neutro en los grupos
Demostrar con Lean4 que un grupo sólo posee un elemento neutro.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] example (e : G) (h : ∀ x, x * e = x) : e = 1 := sorry |
1. Demostración en lenguaje natural
Sea \(e ∈ G\) tal que
\[ (∀ x)[x·e = x] \tag{1} \]
Entonces,
\begin{align}
e &= 1.e &&\text{[porque 1 es neutro]} \\
&= 1 &&\text{[por (1)]}
\end{align}
2. Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 |
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] -- 1ª demostración -- =============== example (e : G) (h : ∀ x, x * e = x) : e = 1 := calc e = 1 * e := (one_mul e).symm _ = 1 := h 1 -- 2ª demostración -- =============== example (e : G) (h : ∀ x, x * e = x) : e = 1 := by have h1 : e = e * e := (h e).symm exact self_eq_mul_left.mp h1 -- 3ª demostración -- =============== example (e : G) (h : ∀ x, x * e = x) : e = 1 := self_eq_mul_left.mp (h e).symm -- 4ª demostración -- =============== example (e : G) (h : ∀ x, x * e = x) : e = 1 := by aesop -- Lemas usados -- ============ -- variable (a b : G) -- #check (one_mul a : 1 * a = a) -- #check (self_eq_mul_left : b = a * b ↔ a = 1) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones con Isabelle/HOL
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 |
theory Unicidad_del_elemento_neutro_en_los_grupos imports Main begin context group begin (* 1ª demostración *) lemma assumes "∀ x. x * e = x" shows "e = 1" proof - have "e = 1 * e" by (simp only: left_neutral) also have "… = 1" using assms by (rule allE) finally show "e = 1" by this qed (* 2ª demostración *) lemma assumes "∀ x. x * e = x" shows "e = 1" proof - have "e = 1 * e" by simp also have "… = 1" using assms by simp finally show "e = 1" . qed (* 3ª demostración *) lemma assumes "∀ x. x * e = x" shows "e = 1" using assms by (metis left_neutral) end end |