Theorems · Theorem · number theory

jacobiSym.value_at

∀ (a : ℤ) {R : Type u_1} [inst : Semiring R] (χ : R →* ℤ),
  (∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p) → ∀ {b : ℕ}, Odd b → jacobiSym a b = χ ↑b

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.

Defined in

Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Cited by

4 results in Mathlib

Foundations

Depth 147 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Semiring