Demostrar con Lean4 que si \(m, n \in \mathbb{N}\) son números naturales, entonces \[\gcd(m, n) = \gcd(n, m)\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (k m n : ℕ) open Nat example : gcd m n = gcd n m := by sorry
Demostrar con Lean4 que si \(x\) divide a \(w\), entonces también divide a \(y(xz)+x^2+w^2\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (w x y z : ℕ) example (h : x ∣ w) : x ∣ y * (x * z) + x^2 + w^2 := by sorry
Demostrar con Lean4 que si \(x, y, z ∈ ℕ\), entonces \(x\) divide a \(yxz\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (x y z : ℕ) example : x ∣ y * x * z := by sorry
Demostrar que los productos de los números naturales por números pares son pares.
Para ello, completar la siguiente teoría de Lean:
import Mathlib.Algebra.Ring.Parity import Mathlib.Tactic open Nat example : ∀ m n : ℕ, Even n → Even (m * n) := by sorry
Si \(n\) es par, entonces (por la definición de Even) existe un \(k\) tal que
\[
\begin{align}
n = k + k && (1)
\end{align}
\]
Por tanto,
\[
\begin{align}
mn &= m(k + k) && (\text{por (1)})\newline
&= mk + mk && (\text{por la propiedad distributiva})
\end{align}
\]
Por consiguiente, \(mn\) es par.
import Mathlib.Algebra.Ring.Parity import Mathlib.Tactic open Nat -- 1ª demostración -- =============== example : ∀ m n : ℕ, Even n → Even (m * n) := by rintro m n ⟨k, hk⟩ use m * k rw [hk] ring -- 2ª demostración -- =============== example : ∀ m n : ℕ, Even n → Even (m * n) := by rintro m n ⟨k, hk⟩ use m * k rw [hk] rw [mul_add] -- 3ª demostración -- =============== example : ∀ m n : ℕ, Even n → Even (m * n) := by rintro m n ⟨k, hk⟩ use m * k rw [hk, mul_add] -- 4ª demostración -- =============== example : ∀ m n : Nat, Even n → Even (m * n) := by rintro m n ⟨k, hk⟩; use m * k; rw [hk, mul_add] -- 5ª demostración -- =============== example : ∀ m n : ℕ, Even n → Even (m * n) := by rintro m n ⟨k, hk⟩ exact ⟨m * k, by rw [hk, mul_add]⟩ -- 6ª demostración -- =============== example : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, hk⟩ ↦ ⟨m * k, by rw [hk, mul_add]⟩ -- 7ª demostración -- =============== example : ∀ m n : ℕ, Even n → Even (m * n) := by rintro m n ⟨k, hk⟩ use m * k rw [hk] exact mul_add m k k -- 8ª demostración -- =============== example : ∀ m n : ℕ, Even n → Even (m * n) := by intros m n hn unfold Even at * cases hn with | intro k hk => use m * k rw [hk, mul_add] -- 9ª demostración -- =============== example : ∀ m n : ℕ, Even n → Even (m * n) := by intros m n hn unfold Even at * cases hn with | intro k hk => use m * k calc m * n = m * (k + k) := by exact congrArg (HMul.hMul m) hk _ = m * k + m * k := by exact mul_add m k k -- 10ª demostración -- ================ example : ∀ m n : Nat, Even n → Even (m * n) := by intros; simp [*, parity_simps] -- Lemas usados -- ============ -- #check (mul_add : ∀ a b c : ℕ, a * (b + c) = a * b + a * c)
Se puede interactuar con las pruebas anteriores en Lean 4 Web.
Demostrar el teorema de Nicómaco que afirma que la suma de los cubos de los \(n\) primeros números naturales es igual que el cuadrado de la suma de los \(n\) primeros números naturales; es decir, para todo número natural n se tiene que \[ 1^3 + 2^3 + ... + n^3 = (1 + 2 + ... + n)^2 \]