even_mul — Mathlib

English

The product m n is even iff at least one of m or n is even.

Русский

Произведение m n чётно тогда, когда хотя бы одно из m,n чётное.

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 mod_two_eq_zero_or_one m with h₁ | h₁ <;> rcases mod_two_eq_zero_or_one n with h₂ | h₂ <;>
    simp [even_iff, h₁, h₂, Nat.mul_mod]

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