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 (n²) es par, entonces (n) es par.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic open Nat variable (n : ℕ) example (h : 2 ∣ n ^ 2) : 2 ∣ n := by sorry
Demostrar con Lean4 que existen infinitos números primos.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic import Mathlib.Data.Nat.Prime.Defs open Nat example (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by sorry
Demostrar con Lean4 que si \(m\) divide a \(n\) o a \(k\), entonces \(m\) divide a \(nk\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {m n k : ℕ} example (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by sorry
Demostrar con Lean4 que 3 divide al máximo común divisor de 6 y 15.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic open Nat example : 3 ∣ gcd 6 15 := by sorry
Demostrar con Lean4 que existen números primos \(m\) y \(n\) tales que \(4 < m < n < 10\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Nat.Prime.Defs import Mathlib.Tactic example : ∃ m n : ℕ, 4 < m ∧ m < n ∧ n < 10 ∧ Nat.Prime m ∧ Nat.Prime n := by sorry
Demostrar con Lean4 que si (m ∣ n ∧ m ≠ n), entonces (m ∣ n ∧ ¬(n ∣ m)).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Nat.GCD.Basic variable {m n : ℕ} example (h : m ∣ n ∧ m ≠ n) : m ∣ n ∧ ¬ n ∣ m := by sorry
Demostrar con Lean4 que si \(a\) divide a \(b\) y a \(c\), entonces divide a \(b+c\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {a b c : ℕ} example (h1 : a ∣ b) (h2 : a ∣ c) : a ∣ (b + c) := by sorry
Demostrar con Lean4 la transitividad de la divisibilidad.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {a b c : ℕ} example (divab : a ∣ b) (divbc : b ∣ c) : a ∣ c := by sorry
Demostrar con Lean4 que si \(x\) e \(y\) son sumas de dos cuadrados, entonces \(xy\) también lo es
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {α : Type _} [CommRing α] variable {x y : α} -- (suma_de_cuadrados x) afirma que x se puede escribir como la suma -- de dos cuadrados. def suma_de_cuadrados (x : α) := ∃ a b, x = a^2 + b^2 example (hx : suma_de_cuadrados x) (hy : suma_de_cuadrados y) : suma_de_cuadrados (x * y) := by sorry