Theorems · Theorem · number theory

legendreSym.quadratic_reciprocity

• #7 of the 100 theorems: Law of Quadratic Reciprocity
• 1000+ list: Quadratic reciprocity theorem

∀ {p q : ℕ} [inst : Fact (Nat.Prime p)] [inst_1 : Fact (Nat.Prime q)],
  p ≠ 2 → q ≠ 2 → p ≠ q → legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))

The Law of Quadratic Reciprocity: if p and q are distinct odd primes, then (q / p) * (p / q) = (-1)^((p-1)(q-1)/4).

Defined in

Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Cited by

1 results in Mathlib

Foundations

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

Assumes

FactFact