Quadratic reciprocity. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main results #
We prove the law of quadratic reciprocity, see legendre_sym.quadratic_reciprocity and
legendre_sym.quadratic_reciprocity', as well as the
interpretations in terms of existence of square roots depending on the congruence mod 4,
zmod.exists_sq_eq_prime_iff_of_mod_four_eq_one, and
zmod.exists_sq_eq_prime_iff_of_mod_four_eq_three.
We also prove the supplementary laws that give conditions for when -1 or 2
(or -2) is a square modulo a prime p:
legendre_sym.at_neg_one and zmod.exists_sq_eq_neg_one_iff for -1,
legendre_sym.at_two and zmod.exists_sq_eq_two_iff for 2,
legendre_sym.at_neg_two and zmod.exists_sq_eq_neg_two_iff for -2.
Implementation notes #
The proofs use results for quadratic characters on arbitrary finite fields
from number_theory.legendre_symbol.quadratic_char.gauss_sum, which in turn are based on
properties of quadratic Gauss sums as provided by number_theory.legendre_symbol.gauss_sum.
Tags #
quadratic residue, quadratic nonresidue, Legendre symbol, quadratic reciprocity
The value of the Legendre symbol at 2 and -2 #
See jacobi_sym.at_two and jacobi_sym.at_neg_two for the corresponding statements
for the Jacobi symbol.
legendre_sym p 2 is given by χ₈ p.
legendre_sym p (-2) is given by χ₈' p.
The Law of Quadratic Reciprocity #
See jacobi_sym.quadratic_reciprocity and variants for a version of Quadratic Reciprocity
for the Jacobi symbol.
The Law of Quadratic Reciprocity: if p and q are distinct odd primes, then
(q / p) * (p / q) = (-1)^((p-1)(q-1)/4).
The Law of Quadratic Reciprocity: if p and q are odd primes and p % 4 = 1,
then (q / p) = (p / q).
The Law of Quadratic Reciprocity: if p and q are primes that are both congruent
to 3 mod 4, then (q / p) = -(p / q).