mod_even_iff — Mathlib

English

If a is even, then n mod a is even iff n is even.

Русский

Если a чётно, то n mod a чётно тогда и только тогда, когда n чётно.

LaTeX

$$$$ \operatorname{Even}(a) \Rightarrow ( \operatorname{Even}(n \bmod a) \iff \operatorname{Even}(n) ). $$$$

Lean4

/-- If `a` is even, then `n` is even iff `n % a` is even. -/
theorem mod_even_iff (ha : Even a) : Even (n % a) ↔ Even n :=
  ((even_sub <| mod_le n a).mp <| even_iff_two_dvd.mpr <| (even_iff_two_dvd.mp ha).trans <| dvd_sub_mod n).symm

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