English
If χ is a multiplicative function χ : R →* ℤ such that J(a | p) = χ(p) for all odd primes p, then J(a | b) = χ(b) for all odd natural numbers b.
Русский
Если χ — мультипликативная функция χ : R →* ℤ такая, что J(a | p) = χ(p) для всех нечётных простых p, то J(a | b) = χ(b) для всех нечётных натуральных b.
LaTeX
$$$ \forall a \in \mathbb{Z}, \; \forall (\chi : R \to^* \mathbb{Z}), \; (\forall p \ (pp : p.Prime), p \neq 2 \Rightarrow legendreSym(p, a) = χ(p)) \Rightarrow (\forall b \text{ odd}, J(a | b) = χ(b)) $$$
Lean4
/-- If `χ` is a multiplicative function such that `J(a | p) = χ p` for all odd primes `p`,
then `J(a | b)` equals `χ b` for all odd natural numbers `b`. -/
theorem value_at (a : ℤ) {R : Type*} [Semiring R] (χ : R →* ℤ)
(hp : ∀ (p : ℕ) (pp : p.Prime), p ≠ 2 → @legendreSym p ⟨pp⟩ a = χ p) {b : ℕ} (hb : Odd b) : J(a | b) = χ b :=
by
conv_rhs => rw [← prod_primeFactorsList hb.pos.ne', cast_list_prod, map_list_prod χ]
rw [jacobiSym, List.map_map, ← List.pmap_eq_map fun _ => prime_of_mem_primeFactorsList]
congr 1; apply List.pmap_congr_left
exact fun p h pp _ => hp p pp (hb.ne_two_of_dvd_nat <| dvd_of_mem_primeFactorsList h)
