Demostrar que los productos de los números naturales por números pares son pares.
Para ello, completar la siguiente teoría de Lean:
import Mathlib.Algebra.Ring.Parity
import Mathlib.Tactic
open Nat
example : ∀ m n : ℕ, Even n → Even (m * n) := by
sorry
Demostración en lenguaje natural
Si \(n\) es par, entonces (por la definición de Even) existe un \(k\) tal que
\[
\begin{align}
n = k + k && (1)
\end{align}
\]
Por tanto,
\[
\begin{align}
mn &= m(k + k) && (\text{por (1)})\newline
&= mk + mk && (\text{por la propiedad distributiva})
\end{align}
\]
Por consiguiente, \(mn\) es par.
Soluciones con Lean4
import Mathlib.Algebra.Ring.Parity
import Mathlib.Tactic
open Nat
-- 1ª demostración
-- ===============
example : ∀ m n : ℕ, Even n → Even (m * n) := by
rintro m n ⟨k, hk⟩
use m * k
rw [hk]
ring
-- 2ª demostración
-- ===============
example : ∀ m n : ℕ, Even n → Even (m * n) := by
rintro m n ⟨k, hk⟩
use m * k
rw [hk]
rw [mul_add]
-- 3ª demostración
-- ===============
example : ∀ m n : ℕ, Even n → Even (m * n) := by
rintro m n ⟨k, hk⟩
use m * k
rw [hk, mul_add]
-- 4ª demostración
-- ===============
example : ∀ m n : Nat, Even n → Even (m * n) := by
rintro m n ⟨k, hk⟩; use m * k; rw [hk, mul_add]
-- 5ª demostración
-- ===============
example : ∀ m n : ℕ, Even n → Even (m * n) := by
rintro m n ⟨k, hk⟩
exact ⟨m * k, by rw [hk, mul_add]⟩
-- 6ª demostración
-- ===============
example : ∀ m n : Nat, Even n → Even (m * n) :=
fun m n ⟨k, hk⟩ ↦ ⟨m * k, by rw [hk, mul_add]⟩
-- 7ª demostración
-- ===============
example : ∀ m n : ℕ, Even n → Even (m * n) := by
rintro m n ⟨k, hk⟩
use m * k
rw [hk]
exact mul_add m k k
-- 8ª demostración
-- ===============
example : ∀ m n : ℕ, Even n → Even (m * n) := by
intros m n hn
unfold Even at *
cases hn with
| intro k hk =>
use m * k
rw [hk, mul_add]
-- 9ª demostración
-- ===============
example : ∀ m n : ℕ, Even n → Even (m * n) := by
intros m n hn
unfold Even at *
cases hn with
| intro k hk =>
use m * k
calc m * n
= m * (k + k) := by exact congrArg (HMul.hMul m) hk
_ = m * k + m * k := by exact mul_add m k k
-- 10ª demostración
-- ================
example : ∀ m n : Nat, Even n → Even (m * n) := by
intros; simp [*, parity_simps]
-- Lemas usados
-- ============
-- #check (mul_add : ∀ a b c : ℕ, a * (b + c) = a * b + a * c)
Se puede interactuar con las pruebas anteriores en Lean 4 Web.
Referencias