mod_even_iff — Mathlib

English

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

Русский

Если a чётно, то n нечётно тогда и только тогда, когда n по модулю a нечётно.

LaTeX

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

Lean4

/-- If `a` is even, then `n` is odd iff `n % a` is odd. -/
theorem mod_even_iff (ha : Even a) : Odd (n % a) ↔ Odd 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

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