Demostrar con Lean4 que un número es par si y solo si lo es su cuadrado.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Group.Even import Mathlib.Tactic open Int variable (n : ℤ) example : Even (n^2) ↔ Even n := by sorry
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