sq_mod_four_eq_one_of_odd — Mathlib

English

If k is odd, then k^2 ≡ 1 mod 4; equivalently k^2 − 1 is divisible by 4, and in fact by 8 when considering refined forms.

Русский

Если k нечетно, то k^2 ≡ 1 mod 4; следовательно, k^2 − 1 кратно 4 (а иногда 8 в уточнённых формулах).

LaTeX

$$$\text{Odd}(k) \Rightarrow k^2 \equiv 1 \pmod{4}.$$$

Lean4

theorem sq_mod_four_eq_one_of_odd {x : ℤ} : Odd x → x ^ 2 % 4 = 1 :=
  by
  intro hx
  unfold Odd at hx
  rcases hx with ⟨_, rfl⟩
  ring_nf
  rw [add_assoc, ← add_mul, Int.add_mul_emod_self_right]
  decide

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