feat(number_theory/legendre_symbol/quadratic_reciprocity): switch to Gauss sum proof, clean-up (#16171)

This PR is (for now) the final step in the quest to change the proof of Quadratic Reciprocity from using the Gauss and Eisenstein lemmas to using the results for quadratic characters of general finite fields obtained from properties of the quadratic Gauss sum. In addition, there is some clean-up of the file and some further results (e.g., on the quadratic character of `-2` and some versions of the law of quadratic reciprocity that are probably easier to use), and the documentation has been extended.

The Gauss and Eisenstein lemmas have been moved to `number_theory/legendre_symbol/gauss_eisenstein_lemmas` (where the auxiliary results needed for them have already been residing).

I have opened a [topic](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2316171.20renovate.20quadratic.20reciprocity/near/294460241) on this under "PR reviews".

Author: MichaelStollBayreuth

archive/imo/imo2008_q3.lean

@@ -33,7 +33,7 @@ lemma p_lemma (p : ℕ) (hpp : nat.prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4]) (h
 begin
   haveI := fact.mk hpp,
   have hp_mod_4_ne_3 : p % 4 ≠ 3, { linarith [(show p % 4 = 1, by exact hp_mod_4_eq_1)] },
-  obtain ⟨y, hy⟩ := (zmod.exists_sq_eq_neg_one_iff p).mpr hp_mod_4_ne_3,
+  obtain ⟨y, hy⟩ := zmod.exists_sq_eq_neg_one_iff.mpr hp_mod_4_ne_3,
 
   let m := zmod.val_min_abs y,
   let n := int.nat_abs m,

src/number_theory/legendre_symbol/gauss_eisenstein_lemmas.lean

@@ -3,8 +3,7 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import field_theory.finite.basic
-import data.zmod.basic
+import number_theory.legendre_symbol.quadratic_reciprocity
 
 /-!
 # Lemmas of Gauss and Eisenstein
@@ -153,6 +152,22 @@ lemma gauss_lemma_aux (p : ℕ) [hp : fact p.prime] [fact (p % 2 = 1)]
           exact nat.div_lt_self hp.1.pos dec_trivial)).1 $
   by simpa using gauss_lemma_aux₁ p hap
 
+/-- Gauss' lemma. The legendre symbol can be computed by considering the number of naturals less
+  than `p/2` such that `(a * x) % p > p / 2` -/
+lemma gauss_lemma {p : ℕ} [fact p.prime] {a : ℤ} (hp : p ≠ 2) (ha0 : (a : zmod p) ≠ 0) :
+  legendre_sym p a = (-1) ^ ((Ico 1 (p / 2).succ).filter
+    (λ x : ℕ, p / 2 < (a * x : zmod p).val)).card :=
+begin
+  haveI hp' : fact (p % 2 = 1) := ⟨nat.prime.mod_two_eq_one_iff_ne_two.mpr hp⟩,
+  have : (legendre_sym p a : zmod p) = (((-1)^((Ico 1 (p / 2).succ).filter
+    (λ x : ℕ, p / 2 < (a * x : zmod p).val)).card : ℤ) : zmod p) :=
+    by { rw [legendre_sym_eq_pow, legendre_symbol.gauss_lemma_aux p ha0]; simp },
+  cases legendre_sym_eq_one_or_neg_one p ha0;
+  cases neg_one_pow_eq_or ℤ ((Ico 1 (p / 2).succ).filter
+    (λ x : ℕ, p / 2 < (a * x : zmod p).val)).card;
+  simp [*, ne_neg_self p one_ne_zero, (ne_neg_self p one_ne_zero).symm] at *
+end
+
 private lemma eisenstein_lemma_aux₁ (p : ℕ) [fact p.prime] [hp2 : fact (p % 2 = 1)]
   {a : ℕ} (hap : (a : zmod p) ≠ 0) :
   ((∑ x in Ico 1 (p / 2).succ, a * x : ℕ) : zmod 2) =
@@ -276,6 +291,17 @@ begin
   simp only [card_Ico, tsub_zero, succ_sub_succ_eq_sub]
 end
 
+lemma eisenstein_lemma {p : ℕ} [fact p.prime] (hp : p ≠ 2) {a : ℕ} (ha1 : a % 2 = 1)
+  (ha0 : (a : zmod p) ≠ 0) :
+  legendre_sym p a = (-1)^∑ x in Ico 1 (p / 2).succ, (x * a) / p :=
+begin
+  haveI hp' : fact (p % 2 = 1) := ⟨nat.prime.mod_two_eq_one_iff_ne_two.mpr hp⟩,
+  have ha0' : ((a : ℤ) : zmod p) ≠ 0 := by { norm_cast, exact ha0 },
+  rw [neg_one_pow_eq_pow_mod_two, gauss_lemma hp ha0', neg_one_pow_eq_pow_mod_two,
+      (by norm_cast : ((a : ℤ) : zmod p) = (a : zmod p)),
+      show _ = _, from legendre_symbol.eisenstein_lemma_aux p ha1 ha0]
+end
+
 end legendre_symbol
 
 end gauss_eisenstein

src/number_theory/legendre_symbol/quadratic_char.lean

@@ -31,7 +31,7 @@ It takes the value zero at zero; for non-zero argument `a : α`, it is `1`
 if `a` is a square, otherwise it is `-1`.
 
 This only deserves the name "character" when it is multiplicative,
-e.g., when `α` is a finite field. See `quadratic_char_mul`.
+e.g., when `α` is a finite field. See `quadratic_char_fun_mul`.
 
 We will later define `quadratic_char` to be a multiplicative character
 of type `mul_char F ℤ`, when the domain is a finite field `F`.
@@ -57,7 +57,7 @@ open mul_char
 variables {F : Type*} [field F] [fintype F] [decidable_eq F]
 
 /-- Some basic API lemmas -/
-lemma quadratic_char_eq_zero_iff' {a : F} : quadratic_char_fun F a = 0 ↔ a = 0 :=
+lemma quadratic_char_fun_eq_zero_iff {a : F} : quadratic_char_fun F a = 0 ↔ a = 0 :=
 begin
   simp only [quadratic_char_fun],
   by_cases ha : a = 0,
@@ -67,15 +67,15 @@ begin
 end
 
 @[simp]
-lemma quadratic_char_zero : quadratic_char_fun F 0 = 0 :=
+lemma quadratic_char_fun_zero : quadratic_char_fun F 0 = 0 :=
 by simp only [quadratic_char_fun, eq_self_iff_true, if_true, id.def]
 
 @[simp]
-lemma quadratic_char_one : quadratic_char_fun F 1 = 1 :=
+lemma quadratic_char_fun_one : quadratic_char_fun F 1 = 1 :=
 by simp only [quadratic_char_fun, one_ne_zero, is_square_one, if_true, if_false, id.def]
 
 /-- If `ring_char F = 2`, then `quadratic_char_fun F` takes the value `1` on nonzero elements. -/
-lemma quadratic_char_eq_one_of_char_two' (hF : ring_char F = 2) {a : F} (ha : a ≠ 0) :
+lemma quadratic_char_fun_eq_one_of_char_two (hF : ring_char F = 2) {a : F} (ha : a ≠ 0) :
   quadratic_char_fun F a = 1 :=
 begin
   simp only [quadratic_char_fun, ha, if_false, ite_eq_left_iff],
@@ -84,34 +84,34 @@ end
 
 /-- If `ring_char F` is odd, then `quadratic_char_fun F a` can be computed in
 terms of `a ^ (fintype.card F / 2)`. -/
-lemma quadratic_char_eq_pow_of_char_ne_two' (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) :
+lemma quadratic_char_fun_eq_pow_of_char_ne_two (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) :
   quadratic_char_fun F a = if a ^ (fintype.card F / 2) = 1 then 1 else -1 :=
 begin
   simp only [quadratic_char_fun, ha, if_false],
   simp_rw finite_field.is_square_iff hF ha,
 end
 
 /-- The quadratic character is multiplicative. -/
-lemma quadratic_char_mul (a b : F) :
+lemma quadratic_char_fun_mul (a b : F) :
   quadratic_char_fun F (a * b) = quadratic_char_fun F a * quadratic_char_fun F b :=
 begin
   by_cases ha : a = 0,
-  { rw [ha, zero_mul, quadratic_char_zero, zero_mul], },
+  { rw [ha, zero_mul, quadratic_char_fun_zero, zero_mul], },
   -- now `a ≠ 0`
   by_cases hb : b = 0,
-  { rw [hb, mul_zero, quadratic_char_zero, mul_zero], },
+  { rw [hb, mul_zero, quadratic_char_fun_zero, mul_zero], },
   -- now `a ≠ 0` and `b ≠ 0`
   have hab := mul_ne_zero ha hb,
   by_cases hF : ring_char F = 2,
   { -- case `ring_char F = 2`
-    rw [quadratic_char_eq_one_of_char_two' hF ha,
-        quadratic_char_eq_one_of_char_two' hF hb,
-        quadratic_char_eq_one_of_char_two' hF hab,
+    rw [quadratic_char_fun_eq_one_of_char_two hF ha,
+        quadratic_char_fun_eq_one_of_char_two hF hb,
+        quadratic_char_fun_eq_one_of_char_two hF hab,
         mul_one], },
   { -- case of odd characteristic
-    rw [quadratic_char_eq_pow_of_char_ne_two' hF ha,
-        quadratic_char_eq_pow_of_char_ne_two' hF hb,
-        quadratic_char_eq_pow_of_char_ne_two' hF hab,
+    rw [quadratic_char_fun_eq_pow_of_char_ne_two hF ha,
+        quadratic_char_fun_eq_pow_of_char_ne_two hF hb,
+        quadratic_char_fun_eq_pow_of_char_ne_two hF hab,
         mul_pow],
     cases finite_field.pow_dichotomy hF hb with hb' hb',
     { simp only [hb', mul_one, eq_self_iff_true, if_true], },
@@ -126,15 +126,19 @@ variables (F)
 /-- The quadratic character as a multiplicative character. -/
 @[simps] def quadratic_char : mul_char F ℤ :=
 { to_fun := quadratic_char_fun F,
-  map_one' := quadratic_char_one,
-  map_mul' := quadratic_char_mul,
-  map_nonunit' := λ a ha, by { rw of_not_not (mt ne.is_unit ha), exact quadratic_char_zero, } }
+  map_one' := quadratic_char_fun_one,
+  map_mul' := quadratic_char_fun_mul,
+  map_nonunit' := λ a ha, by { rw of_not_not (mt ne.is_unit ha), exact quadratic_char_fun_zero, } }
 
 variables {F}
 
 /-- The value of the quadratic character on `a` is zero iff `a = 0`. -/
 lemma quadratic_char_eq_zero_iff {a : F} : quadratic_char F a = 0 ↔ a = 0 :=
-quadratic_char_eq_zero_iff'
+quadratic_char_fun_eq_zero_iff
+
+@[simp]
+lemma quadratic_char_zero : quadratic_char F 0 = 0 :=
+by simp only [quadratic_char_apply, quadratic_char_fun_zero]
 
 /-- For nonzero `a : F`, `quadratic_char F a = 1 ↔ is_square a`. -/
 lemma quadratic_char_one_iff_is_square {a : F} (ha : a ≠ 0) :
@@ -181,15 +185,15 @@ lemma quadratic_char_exists_neg_one (hF : ring_char F ≠ 2) : ∃ a, quadratic_
 /-- If `ring_char F = 2`, then `quadratic_char F` takes the value `1` on nonzero elements. -/
 lemma quadratic_char_eq_one_of_char_two (hF : ring_char F = 2) {a : F} (ha : a ≠ 0) :
   quadratic_char F a = 1 :=
-quadratic_char_eq_one_of_char_two' hF ha
+quadratic_char_fun_eq_one_of_char_two hF ha
 
 /-- If `ring_char F` is odd, then `quadratic_char F a` can be computed in
 terms of `a ^ (fintype.card F / 2)`. -/
 lemma quadratic_char_eq_pow_of_char_ne_two (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) :
   quadratic_char F a = if a ^ (fintype.card F / 2) = 1 then 1 else -1 :=
-quadratic_char_eq_pow_of_char_ne_two' hF ha
+quadratic_char_fun_eq_pow_of_char_ne_two hF ha
 
-lemma quadratic_char_eq_pow_of_char_ne_two'' (hF : ring_char F ≠ 2) (a : F) :
+lemma quadratic_char_eq_pow_of_char_ne_two' (hF : ring_char F ≠ 2) (a : F) :
   (quadratic_char F a : F) = a ^ (fintype.card F / 2) :=
 begin
   by_cases ha : a = 0,
@@ -318,7 +322,7 @@ end
 lemma quadratic_char_two [decidable_eq F] (hF : ring_char F ≠ 2) :
   quadratic_char F 2 = χ₈ (fintype.card F) :=
 is_quadratic.eq_of_eq_coe (quadratic_char_is_quadratic F) is_quadratic_χ₈ hF
-  ((quadratic_char_eq_pow_of_char_ne_two'' hF 2).trans (finite_field.two_pow_card hF))
+  ((quadratic_char_eq_pow_of_char_ne_two' hF 2).trans (finite_field.two_pow_card hF))
 
 /-- `2` is a square in `F` iff `#F` is not congruent to `3` or `5` mod `8`. -/
 lemma finite_field.is_square_two_iff :
@@ -394,7 +398,7 @@ begin
     exact ring.neg_one_ne_one_of_char_ne_two hF', },
   have hχ₂ : χ.is_quadratic := is_quadratic.comp (quadratic_char_is_quadratic F) _,
   have h := char.card_pow_card hχ₁ hχ₂ h hF',
-  rw [← quadratic_char_eq_pow_of_char_ne_two'' hF'] at h,
+  rw [← quadratic_char_eq_pow_of_char_ne_two' hF'] at h,
   exact (is_quadratic.eq_of_eq_coe (quadratic_char_is_quadratic F')
              (quadratic_char_is_quadratic F) hF' h).symm,
 end