Título | Autor |
---|---|
Si x, y, z ∈ ℕ, entonces x divide a yxz |
José A. Alonso |
[mathjax]
Demostrar con Lean4 que si
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
Demostración en lenguaje natural
Por la transitividad de la divisibilidad aplicada a las relaciones \begin{align} x &\mid yx \\ yx &\mid yxz \end{align}
Demostraciones con Lean4
import Mathlib.Data.Real.Basic
variable (x y z : ℕ)
-- 1ª demostración
-- ===============
example : x ∣ y * x * z :=
by
have h1 : x ∣ y * x :=
dvd_mul_left x y
have h2 : (y * x) ∣ (y * x * z) :=
dvd_mul_right (y * x) z
show x ∣ y * x * z
exact dvd_trans h1 h2
-- 2ª demostración
-- ===============
example : x ∣ y * x * z :=
dvd_trans (dvd_mul_left x y) (dvd_mul_right (y * x) z)
-- 3ª demostración
-- ===============
example : x ∣ y * x * z :=
by
apply dvd_mul_of_dvd_left
apply dvd_mul_left
-- Los lemas utilizados son:
#check (dvd_mul_left x y : x ∣ y * x)
#check (dvd_mul_right x y : x ∣ x * y)
#check (dvd_trans : x ∣ y → y ∣ z → x ∣ z)
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 19.