Mathlib Map

Theorems · Definition · number theory

jacobiSym

ℤ → ℕ → ℤ

The Jacobi symbol of a and b

Defined in
Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
Cited by
44 results in Mathlib
Foundations
Depth 145 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

qrSign · cited by 9qrSignjacobiSym.mul_left · cited by 8jacobiSym.mul_leftjacobiSym.one_left · cited by 5jacobiSym.one_leftqrSign.neg_one_pow · cited by 4qrSign.neg_one_powjacobiSym.value_at · cited by 4jacobiSym.value_atjacobiSym.zero_right · cited by 4jacobiSym.zero_rightjacobiSym.eq_zero_iff_not_coprime · cited by 3jacobiSym.eq_zero_iff_not…jacobiSym.mod_left · cited by 3jacobiSym.mod_leftjacobiSym.pow_left · cited by 3jacobiSym.pow_leftjacobiSym.legendreSym.to_jacobiSym · cited by 3legendreSym.to_jacobiSymjacobiSym.at_neg_one · cited by 2jacobiSym.at_neg_onejacobiSym.at_two · cited by 2jacobiSym.at_twojacobiSym.mul_right · cited by 2jacobiSym.mul_rightjacobiSym.mul_right' · cited by 2jacobiSym.mul_right'jacobiSym.ne_zero · cited by 2jacobiSym.ne_zeroNat.Prime · cited by 2059Nat.PrimeNat.primeFactorsList · cited by 105Nat.primeFactorsListlegendreSym · cited by 51legendreSymNat.prime_of_mem_primeFactorsList · cited by 30Nat.prime_of_mem_primeFac…jacobiSymCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by45

Results whose statement or proof uses this declaration.