Divisibilidad – Calculemus

Conmutatividad del máximo común divisor

PorJosé A. Alonso 14 septiembre 202330 agosto 2023

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

import Mathlib.Data.Real.Basic

variable (k m n : ℕ)

open Nat

example : gcd m n = gcd n m :=

by sorry

Si x divide a w, entonces también divide a y(xz)+x²+w²

PorJosé A. Alonso 13 septiembre 202324 agosto 2023

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

import Mathlib.Data.Real.Basic

variable (w x y z : ℕ)

example

(h : x ∣ w)

: x ∣ y * (x * z) + x^2 + w^2 :=

by sorry

Si x, y, z ∈ ℕ, entonces x divide a yxz

PorJosé A. Alonso 12 septiembre 202325 septiembre 2023

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

import Mathlib.Data.Real.Basic

variable (x y z : ℕ)

example : x ∣ y * x * z :=

by sorry

Si w, x, y, z ∈ ℕ tales que x ∣ w, entonces x ∣ yxz + x² + w²

PorJosé A. Alonso 10 octubre 20224 octubre 2022

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:

import data.nat.gcd

variables w x y z : ℕ

example
  (h : x ∣ w)
  : x ∣ y * (x * z) + x^2 + w^2 :=
sorry

import data.nat.gcd

variables w x y z : ℕ

example

(h : x ∣ w)

: x ∣ y * (x * z) + x^2 + w^2 :=

sorry

Si x ∈ ℕ, entonces x ∣ x²

PorJosé A. Alonso 7 octubre 202227 septiembre 2022

Demostrar que si x ∈ ℕ, entonces

x ∣ x^2

x ∣ x^2

Para ello, completar la siguiente teoría de Lean:

import data.nat.pow
variable x : ℕ

example : x ∣ x^2 :=
sorry

import data.nat.pow

variable x : ℕ

example : x ∣ x^2 :=

sorry

Read More «Si x ∈ ℕ, entonces x ∣ x²»

Si x, y, z ∈ ℕ, entonces x ∣ y * x * z

PorJosé A. Alonso 6 octubre 202226 septiembre 2022

Demostrar que si x, y, z ∈ N, entonces

   x ∣ y * x * z

1	x ∣ y * x * z

Para ello, completar la siguiente teoría de Lean:

import data.nat.basic
variables x y z : ℕ

example : x ∣ y * x * z :=
sorry

import data.nat.basic

variables x y z : ℕ

example : x ∣ y * x * z :=

sorry

El producto por un par es par

PorJosé A. Alonso 21 agosto 202211 septiembre 2022

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 data.nat.parity
import tactic

open nat

example : ∀ m n : ℕ, even n → even (m * n) :=
sorry

import data.nat.parity

import tactic

open nat

example : ∀ m n : ℕ, even n → even (m * n) :=

sorry