Demostrar con Lean4 que si \(x, y, z \u2208 \u2115\), entonces \(x\) divide a \(yxz\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\nvariable (x y z : \u2115)\n\nexample : x \u2223 y * x * z :=\nby sorry\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Por la transitividad de la divisibilidad aplicada a las relaciones
\n\\begin{align}
\n x &\\mid yx \\
\n yx &\\mid yxz
\n\\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\nimport Mathlib.Data.Real.Basic\nvariable (x y z : \u2115)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2223 y * x * z :=\nby\n have h1 : x \u2223 y * x :=\n dvd_mul_left x y\n have h2 : (y * x) \u2223 (y * x * z) :=\n dvd_mul_right (y * x) z\n show x \u2223 y * x * z\n exact dvd_trans h1 h2\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2223 y * x * z :=\ndvd_trans (dvd_mul_left x y) (dvd_mul_right (y * x) z)\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : x \u2223 y * x * z :=\nby\n apply dvd_mul_of_dvd_left\n apply dvd_mul_left\n\n\n-- Los lemas utilizados son:\n#check (dvd_mul_left x y : x \u2223 y * x)\n#check (dvd_mul_right x y : x \u2223 x * y)\n#check (dvd_trans : x \u2223 y \u2192 y \u2223 z \u2192 x \u2223 z)\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n