odd_mod_four_iff — Mathlib

English

An integer is odd iff its remainder mod 4 is 1 or 3.

Русский

Число нечётно тогда и только тогда, когда остаток от деления на 4 равен 1 или 3.

LaTeX

$$$ n \equiv 1 \pmod{2} \iff (n \equiv 1 \pmod{4} \lor n \equiv 3 \pmod{4}) $$$

Lean4

/-- A natural number is odd iff it has residue `1` or `3` mod `4`. -/
theorem odd_mod_four_iff {n : ℕ} : n % 2 = 1 ↔ n % 4 = 1 ∨ n % 4 = 3 :=
  have help : ∀ m : ℕ, m < 4 → m % 2 = 1 → m = 1 ∨ m = 3 := by decide
  ⟨fun hn => help (n % 4) (mod_lt n (by cutsat)) <| (mod_mod_of_dvd n (by decide : 2 ∣ 4)).trans hn, fun h =>
    Or.elim h odd_of_mod_four_eq_one odd_of_mod_four_eq_three⟩

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