even_mul — Mathlib

English

For integers m,n, m n is even if and only if m is even or n is even.

Русский

Для целых чисел m,n чётность произведения mn равна нулю, если хотя бы одно из множителей чётно.

LaTeX

$$$$ \operatorname{Even}(m n) \iff \operatorname{Even}(m) \lor \operatorname{Even}(n). $$$$

Lean4

@[parity_simps, grind =]
theorem even_mul : Even (m * n) ↔ Even m ∨ Even n := by
  rcases emod_two_eq_zero_or_one m with h₁ | h₁ <;> rcases emod_two_eq_zero_or_one n with h₂ | h₂ <;>
    simp [even_iff, h₁, h₂, Int.mul_emod]

Похожие утверждения