mathlib3documentation

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 #

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.

theorem legendre_sym.at_two {p : } [fact (nat.prime p)] (hp : p 2) :
2 =

legendre_sym p 2 is given by χ₈ p.

theorem legendre_sym.at_neg_two {p : } [fact (nat.prime p)] (hp : p 2) :
(-2) =

legendre_sym p (-2) is given by χ₈' p.

theorem zmod.exists_sq_eq_two_iff {p : } [fact (nat.prime p)] (hp : p 2) :
p % 8 = 1 p % 8 = 7

2 is a square modulo an odd prime p iff p is congruent to 1 or 7 mod 8.

theorem zmod.exists_sq_eq_neg_two_iff {p : } [fact (nat.prime p)] (hp : p 2) :
is_square (-2) p % 8 = 1 p % 8 = 3

-2 is a square modulo an odd prime p iff p is congruent to 1 or 3 mod 8.

The Law of Quadratic Reciprocity #

See jacobi_sym.quadratic_reciprocity and variants for a version of Quadratic Reciprocity for the Jacobi symbol.

theorem legendre_sym.quadratic_reciprocity {p q : } [fact (nat.prime p)] [fact (nat.prime q)] (hp : p 2) (hq : q 2) (hpq : 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).

theorem legendre_sym.quadratic_reciprocity' {p q : } [fact (nat.prime p)] [fact (nat.prime q)] (hp : p 2) (hq : q 2) :
= (-1) ^ (p / 2 * (q / 2)) *

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

theorem legendre_sym.quadratic_reciprocity_one_mod_four {p q : } [fact (nat.prime p)] [fact (nat.prime q)] (hp : p % 4 = 1) (hq : q 2) :
=

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

theorem legendre_sym.quadratic_reciprocity_three_mod_four {p q : } [fact (nat.prime p)] [fact (nat.prime q)] (hp : p % 4 = 3) (hq : q % 4 = 3) :
= -

The Law of Quadratic Reciprocity: if p and q are primes that are both congruent to 3 mod 4, then (q / p) = -(p / q).

theorem zmod.exists_sq_eq_prime_iff_of_mod_four_eq_one {p q : } [fact (nat.prime p)] [fact (nat.prime q)] (hp1 : p % 4 = 1) (hq1 : q 2) :

If p and q are odd primes and p % 4 = 1, then q is a square mod p iff p is a square mod q.

theorem zmod.exists_sq_eq_prime_iff_of_mod_four_eq_three {p q : } [fact (nat.prime p)] [fact (nat.prime q)] (hp3 : p % 4 = 3) (hq3 : q % 4 = 3) (hpq : p q) :

If p and q are distinct primes that are both congruent to 3 mod 4, then q is a square mod p iff p is a nonsquare mod q.