Demostrar con Lean4 que si \\(m\\) divide a \\(n\\) o a \\(k\\), entonces \\(m\\) divide a \\(nk\\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\r\nimport Mathlib.Tactic\r\nvariable {m n k : \u2115}\r\n\r\nexample\r\n (h : m \u2223 n \u2228 m \u2223 k)\r\n : m \u2223 n * k :=\r\nby sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Se demuestra por casos.<\/p>\n
Caso 1: Supongamos que \\(m \u2223 n\\). Entonces, existe un \\(a \u2208 \u2115\\) tal que
\n\\[ n = ma \\]
\nPor tanto,
\n\\begin{align}
\n nk &= (ma)k \\\\
\n &= m(ak)
\n\\end{align}
\nque es divisible por \\(m\\).<\/p>\n
Caso 2: Supongamos que \\(m \u2223 k). Entonces, existe un \\(b \u2208 \u2115\\) tal que
\n\\[ k = mb \\]
\nPor tanto,
\n\\begin{align}
\n nk &= n(mb) \\\\
\n &= m(nb)
\n\\end{align}
\nque es divisible por \\(m\\).<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Tactic\r\nvariable {m n k : \u2115}\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : m \u2223 n \u2228 m \u2223 k)\r\n : m \u2223 n * k :=\r\nby\r\n rcases h with h1 | h2\r\n . -- h1 : m \u2223 n\r\n rcases h1 with \u27e8a, ha\u27e9\r\n -- a : \u2115\r\n -- ha : n = m * a\r\n rw [ha]\r\n -- \u22a2 m \u2223 (m * a) * k\r\n rw [mul_assoc]\r\n -- \u22a2 m \u2223 m * (a * k)\r\n exact dvd_mul_right m (a * k)\r\n . -- h2 : m \u2223 k\r\n rcases h2 with \u27e8b, hb\u27e9\r\n -- b : \u2115\r\n -- hb : k = m * b\r\n rw [hb]\r\n -- \u22a2 m \u2223 n * (m * b)\r\n rw [mul_comm]\r\n -- \u22a2 m \u2223 (m * b) * n\r\n rw [mul_assoc]\r\n -- \u22a2 m \u2223 m * (b * n)\r\n exact dvd_mul_right m (b * n)\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : m \u2223 n \u2228 m \u2223 k)\r\n : m \u2223 n * k :=\r\nby\r\n rcases h with h1 | h2\r\n . -- h1 : m \u2223 n\r\n rcases h1 with \u27e8a, ha\u27e9\r\n -- a : \u2115\r\n -- ha : n = m * a\r\n rw [ha, mul_assoc]\r\n -- \u22a2 m \u2223 m * (a * k)\r\n exact dvd_mul_right m (a * k)\r\n . -- h2 : m \u2223 k\r\n rcases h2 with \u27e8b, hb\u27e9\r\n -- b : \u2115\r\n -- hb : k = m * b\r\n rw [hb, mul_comm, mul_assoc]\r\n -- \u22a2 m \u2223 m * (b * n)\r\n exact dvd_mul_right m (b * n)\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : m \u2223 n \u2228 m \u2223 k)\r\n : m \u2223 n * k :=\r\nby\r\n rcases h with \u27e8a, rfl\u27e9 | \u27e8b, rfl\u27e9\r\n . -- a : \u2115\r\n -- \u22a2 m \u2223 (m * a) * k\r\n rw [mul_assoc]\r\n -- \u22a2 m \u2223 m * (a * k)\r\n exact dvd_mul_right m (a * k)\r\n . -- \u22a2 m \u2223 n * (m * b)\r\n rw [mul_comm, mul_assoc]\r\n -- \u22a2 m \u2223 m * (b * n)\r\n exact dvd_mul_right m (b * n)\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\n-- ===============\r\n\r\nexample\r\n (h : m \u2223 n \u2228 m \u2223 k)\r\n : m \u2223 n * k :=\r\nby\r\n rcases h with h1 | h2\r\n . -- h1 : m \u2223 n\r\n exact dvd_mul_of_dvd_left h1 k\r\n . -- h2 : m \u2223 k\r\n exact dvd_mul_of_dvd_right h2 n\r\n\r\n-- Lemas usados\r\n-- ============\r\n\r\n-- #check (dvd_mul_of_dvd_left : m \u2223 n \u2192 \u2200 (c : \u2115), m \u2223 n * c)\r\n-- #check (dvd_mul_of_dvd_right : m \u2223 n \u2192 \u2200 (c : \u2115), m \u2223 c * n)\r\n-- #check (dvd_mul_right m n : m \u2223 m * n)\r\n-- #check (mul_assoc m n k : m * n * k = m * (n * k))\r\n-- #check (mul_comm m n : m * n = n * m)\r\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n