Si x, y, z ∈ ℕ, entonces x ∣ y * x * z
Demostrar que si x, y, z ∈ N, entonces
|
1 |
x ∣ y * x * z |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 |
import data.nat.basic variables x y z : ℕ example : x ∣ y * x * z := sorry |
Soluciones con Lean
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 |
import data.nat.basic variables x y z : ℕ -- 1ª demostración -- =============== example : x ∣ y * x * z := begin have h1 : x ∣ y * x, { exact dvd_mul_left x y }, have h2 : (y * x) ∣ (y * x * z), { exact dvd.intro z rfl}, show x ∣ y * x * z, { exact dvd_trans h1 h2}, end -- 2ª demostración -- =============== example : x ∣ y * x * z := dvd_trans (dvd_mul_left x y) (dvd.intro z rfl) -- 3ª demostración -- =============== example : x ∣ y * x * z := begin apply dvd_mul_of_dvd_left, apply dvd_mul_left end |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 20.
