English
For a ∈ ℤ and b ∈ ℕ with b odd, J(a|b) = J(a| b mod (4|a|)).
Русский
Для a ∈ ℤ и b ∈ ℕ с b нечетно, J(a|b) = J(a| b mod (4|a|)).
LaTeX
$$$\forall a \in \mathbb{Z},\forall b \in \mathbb{N},\text{Odd}(b) \Rightarrow J(a|b) = J\bigl(a| (b \bmod (4 \cdot |a|))\bigr)$$$
Lean4
/-- The Jacobi symbol `J(a | b)` depends only on `b` mod `4*a`. -/
theorem mod_right (a : ℤ) {b : ℕ} (hb : Odd b) : J(a | b) = J(a | b % (4 * a.natAbs)) :=
by
rcases Int.natAbs_eq a with ha | ha <;> nth_rw 2 [ha] <;> nth_rw 1 [ha]
· exact mod_right' a.natAbs hb
· have hb' : Odd (b % (4 * a.natAbs)) := hb.mod_even (Even.mul_right (by decide) _)
rw [jacobiSym.neg _ hb, jacobiSym.neg _ hb', mod_right' _ hb, χ₄_nat_mod_four, χ₄_nat_mod_four (b % (4 * _)),
mod_mod_of_dvd b (dvd_mul_right 4 _)]
