English
The Jacobi symbol J(a|b) depends only on b modulo 4a when b is odd.
Русский
Символ Якоби J(a|b) зависит только от b по модулю 4a, если b нечетно.
LaTeX
$$$\forall a \in \mathbb{N},\forall b \in \mathbb{N},\ \text{Odd}(b) \Rightarrow J(a|b) = J(a|b \bmod (4a))$$$
Lean4
theorem quadratic_reciprocity_if {a b : ℕ} (ha2 : a % 2 = 1) (hb2 : b % 2 = 1) :
(if a % 4 = 3 ∧ b % 4 = 3 then -J(b | a) else J(b | a)) = J(a | b) :=
by
rcases Nat.odd_mod_four_iff.mp ha2 with ha1 | ha3
· simpa [ha1] using jacobiSym.quadratic_reciprocity_one_mod_four' (Nat.odd_iff.mpr hb2) ha1
rcases Nat.odd_mod_four_iff.mp hb2 with hb1 | hb3
· simpa [hb1] using jacobiSym.quadratic_reciprocity_one_mod_four hb1 (Nat.odd_iff.mpr ha2)
simpa [ha3, hb3] using (jacobiSym.quadratic_reciprocity_three_mod_four ha3 hb3).symm