Ir al contenido principal

Publicaciones sobre Números naturales

Canal RSS (Números naturales, es)

Si n² es par, entonces n es par

Teoría de números/Números naturales

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

Leer más…

Si m divide a n o a k, entonces m divide a nk.

Teoría de números/Números naturales

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

Leer más…

3 divide al máximo común divisor de 6 y 15

Teoría de números/Números naturales

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

Leer más…

Existen números primos m y n tales que 4 < m < n < 10

Teoría de números/Números naturales

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

Leer más…

Si a divide a b y a c, entonces divide a b+c

Teoría de números/Números naturales

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

Leer más…

Transitividad de la divisibilidad

Teoría de números/Números naturales

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

Leer más…

Si x e y son sumas de dos cuadrados, entonces xy también lo es

Teoría de números/Números naturales

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

Leer más…

El producto por un par es par

Teoría de números/Números naturales

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

Demostración en lenguaje natural

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.

Soluciones con Lean4

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.

Referencias