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:
|
1 2 3 4 5 6 7 |
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:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable (w x y z : ℕ) example (h : x ∣ w) : x ∣ y * (x * z) + x^2 + w^2 := by sorry |
Read More «Si x divide a w, entonces también divide a y(xz)+x²+w²»
Demostrar con Lean4 que si \(x, y, z ∈ ℕ\), entonces \(x\) divide a \(yxz\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable (x y z : ℕ) example : x ∣ y * x * z := by sorry |
Demostrar que Si w, x, y, z ∈ ℕ tales que x ∣ w, entonces x ∣ yxz + x² + w²
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 |
import data.nat.gcd variables w x y z : ℕ example (h : x ∣ w) : x ∣ y * (x * z) + x^2 + w^2 := sorry |
Read More «Si w, x, y, z ∈ ℕ tales que x ∣ w, entonces x ∣ yxz + x² + w²»
Demostrar que si x ∈ ℕ, entonces
|
1 |
x ∣ x^2 |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 |
import data.nat.pow variable x : ℕ example : x ∣ x^2 := sorry |
Demostrar que si x, y, z ∈ N, entonces
|
1 |
x ∣ y * x * z |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 |
import data.nat.basic variables x y z : ℕ example : x ∣ y * x * z := 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:
|
1 2 3 4 5 6 7 |
import data.nat.parity import tactic open nat example : ∀ m n : ℕ, even n → even (m * n) := sorry |