Demostrar que los productos de los n\u00fameros naturales por n\u00fameros pares son pares.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\r\nimport Mathlib.Data.Nat.Basic\r\nimport Mathlib.Data.Nat.Parity\r\nimport Mathlib.Tactic\r\n\r\nopen Nat\r\n\r\nexample : \u2200 m n : \u2115, Even n \u2192 Even (m * n) := by\r\n sorry\r\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nSi \\(n\\) es par, entonces (por la definici\u00f3n de `Even`) existe un \\(k\\) tal que
\n\\[
\n\\begin{align*}
\nn = k + k && (1)
\n\\end{align*}
\n\\]
\nPor tanto,
\n\\[
\n\\begin{align*}
\n mn &= m(k + k) && (\\text{por (1)})\\\\
\n &= mk + mk && (\\text{por la propiedad distributiva})
\n\\end{align*}
\n\\]
\nPor consiguiente, \\(mn\\) es par.<\/p>\n
Soluciones con Lean4<\/b><\/p>\n\r\nimport Mathlib.Data.Nat.Basic\r\nimport Mathlib.Data.Nat.Parity\r\nimport Mathlib.Tactic\r\n\r\nopen Nat\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample : \u2200 m n : \u2115, Even n \u2192 Even (m * n) := by\r\n rintro m n \u27e8k, hk\u27e9\r\n use m * k\r\n rw [hk]\r\n ring\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample : \u2200 m n : \u2115, Even n \u2192 Even (m * n) := by\r\n rintro m n \u27e8k, hk\u27e9\r\n use m * k\r\n rw [hk]\r\n rw [mul_add]\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : \u2200 m n : \u2115, Even n \u2192 Even (m * n) := by\r\n rintro m n \u27e8k, hk\u27e9\r\n use m * k\r\n rw [hk, mul_add]\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample : \u2200 m n : Nat, Even n \u2192 Even (m * n) := by\r\n rintro m n \u27e8k, hk\u27e9; use m * k; rw [hk, mul_add]\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample : \u2200 m n : \u2115, Even n \u2192 Even (m * n) := by\r\n rintro m n \u27e8k, hk\u27e9\r\n exact \u27e8m * k, by rw [hk, mul_add]\u27e9\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample : \u2200 m n : Nat, Even n \u2192 Even (m * n) :=\r\nfun m n \u27e8k, hk\u27e9 \u21a6 \u27e8m * k, by rw [hk, mul_add]\u27e9\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\nexample : \u2200 m n : \u2115, Even n \u2192 Even (m * n) := by\r\n rintro m n \u27e8k, hk\u27e9\r\n use m * k\r\n rw [hk]\r\n exact mul_add m k k\r\n\r\n-- 8\u00aa demostraci\u00f3n\r\nexample : \u2200 m n : \u2115, Even n \u2192 Even (m * n) := by\r\n intros m n hn\r\n unfold Even at *\r\n cases hn with\r\n | intro k hk =>\r\n use m * k\r\n rw [hk, mul_add]\r\n\r\n-- 9\u00aa demostraci\u00f3n\r\nexample : \u2200 m n : \u2115, Even n \u2192 Even (m * n) := by\r\n intros m n hn\r\n unfold Even at *\r\n cases hn with\r\n | intro k hk =>\r\n use m * k\r\n calc m * n\r\n = m * (k + k) := by exact congrArg (HMul.hMul m) hk\r\n _ = m * k + m * k := by exact mul_add m k k\r\n\r\n-- 10\u00aa demostraci\u00f3n\r\nexample : \u2200 m n : Nat, Even n \u2192 Even (m * n) := by\r\n intros; simp [*, parity_simps]\r\n<\/pre>\nSe puede interactuar con las pruebas anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n