Public Mathlib landmark · existing upstream theorem · read-only
ProofAtlas

Number theory · existing Mathlib theorem

Quadratic Reciprocity

For two distinct odd primes p and q, whether q is a square modulo p and whether p is a square modulo q are linked. Their Legendre symbols multiply to a sign determined by the parities encoded by p divided by 2 and q divided by 2.

Four separate status axes

Upstream indexedPinned source bytes verified locally
Locally reproducedExact upstream declaration replayed
Reviewed pageCurrent public presentation reviewed
Accepted Atlas resultNot recorded for the preferred artifact

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

Formal orientation

Statement map

Statement map for Quadratic ReciprocityFor distinct odd primes, the two Legendre symbols are related by the quadratic-reciprocity sign. The pinned upstream declaration is legendreSym.quadratic_reciprocity. The exact checked statement is legendreSym.quadratic_reciprocity {p q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) : legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2)).Mathematical readingFor distinct odd primes,the two Legendre symbolsare related by thequadratic-reciprocitysign.Pinned declarationmathlib ·legendreSym.quadratic_reciprocityExact checked formlegendreSym.quadratic_reciprocity{p q : ℕ} [Fact(Nat.Prime p)] [Fact(Nat.Prime q)] (hp : p ≠2) (hq : q ≠ 2) (hpq : p≠ q) : legendreSym q ↑p* legendreSym p ↑q =(-1) ^ (p / 2 * (q / 2))Statement map for Quadratic ReciprocityFor distinct odd primes, the two Legendre symbols are related by the quadratic-reciprocity sign. The pinned upstream declaration is legendreSym.quadratic_reciprocity. The exact checked statement is legendreSym.quadratic_reciprocity {p q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) : legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2)).Mathematical readingFor distinct odd primes,the two Legendre symbolsare related by thequadratic-reciprocitysign.Pinned declarationmathlib ·legendreSym.quadratic_reciprocityExact checked formlegendreSym.quadratic_reciprocity{p q : ℕ} [Fact(Nat.Prime p)] [Fact(Nat.Prime q)] (hp : p ≠2) (hq : q ≠ 2) (hpq : p≠ q) : legendreSym q ↑p* legendreSym p ↑q =(-1) ^ (p / 2 * (q / 2))

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

The theorem at a glance

Quadratic Reciprocity at a glance

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

The reciprocal Legendre-symbol product has one exact parity-controlled sign, with p divided by 2 and q divided by 2 interpreted by natural-number floor division. Generated explanation only; the exact HTML statement and pinned source are authoritative.
Detailed visual description

Green and blue prime medallions face each other across reciprocal arcs. A central formula gives the Legendre-symbol product and its sign exponent. Below it, the poster explicitly says natural division rounds down and separates the both-3-mod-4 minus case from the otherwise-plus case.

Quadratic residue information in two odd distinct primes is linked in both directions, with a parity-controlled sign. Generated explanation only; the exact HTML statement and pinned source are authoritative.
Detailed visual description

Two large symmetric residue circles face each other across reciprocal gold arrows. Smaller paired circles below show one aligned exchange and one restrained red reversal cue, suggesting the parity-dependent sign without rendering notation.

Complementary intuition

A mathematical landmark

Quadratic reciprocity is a central symmetry law of elementary number theory. It turns one quadratic-residue question into another, with an exact sign correction.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

legendreSym.quadratic_reciprocity {p q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) : legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
Selected evidence declaration text
theorem legendreSym.quadratic_reciprocity {p q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) : legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))

Proof architecture

How quadratic characters yield reciprocity

4 curated stages

Mathlib's checked route prepares odd-prime field inputs, invokes its finite-field quadratic-character reciprocity identity, cancels the squared nonzero character factor, and evaluates the remaining parity signs.

These source-anchored stages explain the retained Mathlib proof route. They are generated explanations, not proof evidence or an extracted Lean proof-term dependency graph.

  1. Prepare the odd-prime inputs

    The non-two hypotheses supply the oddness and characteristic facts required by the quadratic-character identity.

    Odd p ∧ Odd q ∧ ringChar (ZMod q) ≠ 2

    Primality together with p ≠ 2 and q ≠ 2 supplies oddness for both primes, while the ZMod characteristic calculation supplies the non-characteristic-two input used later. The distinctness hypothesis is retained for the cross-field nonzero argument.

  2. Invoke quadratic-character reciprocity

    Mathlib's finite-field quadratic-character reciprocity lemma supplies the central cross-field relation.

    h := quadraticChar_odd_prime ...

    The proof applies quadraticChar_odd_prime to ZMod p and the odd prime q, using p ≠ q to keep the transported element nonzero. After rewriting the cardinality of ZMod p, this becomes the relation that the remaining rewrites normalize.

  3. Normalize and cancel the square

    Unfolding the Legendre symbols exposes multiplicative quadratic characters, and the squared nonzero character factor collapses to one.

    quadraticChar (ZMod q) p ^ 2 = 1

    The final rewrite chain expands both Legendre symbols, aligns the natural and integer casts, substitutes the reciprocity relation, rotates the product, and uses quadraticChar_sq_one with prime_ne_zero. This algebraic cancellation leaves only parity-controlled sign factors.

  4. Evaluate the reciprocity sign

    Oddness evaluates the two character signs and leaves exactly the parity-controlled sign in quadratic reciprocity.

    legendreSym q p * legendreSym p q = (-1) ^ (p / 2 * (q / 2))

    The proof uses χ₄'s odd-input evaluation for p and q together with quadraticChar_neg_one in ZMod q. The exponent rewrites combine the two parity contributions and close the exact Legendre-symbol product stated by quadratic_reciprocity.

Claim boundary

No new theorem is claimed

This page states Mathlib's Legendre-symbol formulation for primes supplied through Fact instances, with explicit exclusions p ≠ 2, q ≠ 2, and p ≠ q. It does not present the Jacobi-symbol variants or remove those hypotheses.

Provenance

Origin and evidence stay separate

Existing declaration
legendreSym.quadratic_reciprocity in mathlib
Relationship
The checked artifact is the upstream declaration itself
Preferred checked artifact
artifact.library.mathlib.quadratic-reciprocity.v001
Source handling
Verified upstream reference; no mirrored source package