English
The Jacobi symbol J(a|b) is defined as the product, over all prime factors p of b, of the Legendre symbol (a|p).
Русский
Символ Якоби J(a|b) задаётся как произведение Лежандровых символов (a|p) по всем простым делителям p числа b (с учётом кратностей).
LaTeX
$$$\operatorname{jacobiSym}(a,b) = \prod_{p \mid b} \operatorname{legendreSym}(p,a)^{\nu_p(b)}$$$
Lean4
/-- The Jacobi symbol is multiplicative in its first argument. -/
theorem mul_left (a₁ a₂ : ℤ) (b : ℕ) : J(a₁ * a₂ | b) = J(a₁ | b) * J(a₂ | b) :=
by
simp_rw [jacobiSym, List.pmap_eq_map_attach, legendreSym.mul _ _ _]
exact
List.prod_map_mul (l := (primeFactorsList b).attach) (f := fun x ↦
@legendreSym x { out := prime_of_mem_primeFactorsList x.2 } a₁) (g := fun x ↦
@legendreSym x { out := prime_of_mem_primeFactorsList x.2 } a₂)
