refactor(number_theory/legendre_symbol/quadratic_reciprocity.lean): c…

…hange definition of legendre_sym, simplify proofs, add lemmas (#13667)

This changes the definition of `legendre_sym` to use `quadratic_char`.
The proof of some of the statements can then be simplified by using the corresponding statements for quadratic characters.
Some new API lemmas are added, including the fact that the Legendre symbol is multiplicative,

Also, a few `simps` are squeezed in `.../quadratic_char.lean`.

src/data/zmod/basic.lean

@@ -151,6 +151,10 @@ instance (n : ℕ) : char_p (zmod n) n :=
     rw [val_nat_cast, val_zero, nat.dvd_iff_mod_eq_zero],
   end }
 
+/-- We have that `ring_char (zmod n) = n`. -/
+lemma ring_char_zmod_n (n : ℕ) : ring_char (zmod n) = n :=
+by { rw ring_char.eq_iff, exact zmod.char_p n, }
+
 @[simp] lemma nat_cast_self (n : ℕ) : (n : zmod n) = 0 :=
 char_p.cast_eq_zero (zmod n) n
 

src/number_theory/legendre_symbol/quadratic_char.lean

@@ -72,7 +72,7 @@ end
 
 /-- A unit `a` of a finite field `F` of odd characteristic is a square
 if and only if `a ^ (#F / 2) = 1`. -/
-lemma unit_is_sqare_iff (hF : ring_char F ≠ 2) (a : Fˣ) :
+lemma unit_is_square_iff (hF : ring_char F ≠ 2) (a : Fˣ) :
   is_square a ↔ a ^ (fintype.card F / 2) = 1 :=
 begin
   classical,
@@ -102,7 +102,7 @@ lemma is_square_iff (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) :
   is_square a ↔ a ^ (fintype.card F / 2) = 1 :=
 begin
   apply (iff_congr _ (by simp [units.ext_iff])).mp
-        (finite_field.unit_is_sqare_iff hF (units.mk0 a ha)),
+        (finite_field.unit_is_square_iff hF (units.mk0 a ha)),
   simp only [is_square, units.ext_iff, units.coe_mk0, units.coe_mul],
   split, { rintro ⟨y, hy⟩, exact ⟨y, hy⟩ },
   { rintro ⟨y, rfl⟩,
@@ -176,7 +176,7 @@ begin
   simp only [quadratic_char],
   by_cases ha : a = 0,
   { simp only [ha, eq_self_iff_true, if_true], },
-  { simp [ha],
+  { simp only [ha, if_false, iff_false],
     split_ifs; simp only [neg_eq_zero, one_ne_zero, not_false_iff], },
 end
 
@@ -191,7 +191,8 @@ by simp only [quadratic_char, one_ne_zero, is_square_one, if_true, if_false, id.
 /-- For nonzero `a : F`, `quadratic_char F a = 1 ↔ is_square a`. -/
 lemma quadratic_char_one_iff_is_square {a : F} (ha : a ≠ 0) :
   quadratic_char F a = 1 ↔ is_square a :=
-by { simp [quadratic_char, ha, (dec_trivial : (-1 : ℤ) ≠ 1)], tauto }
+by { simp only [quadratic_char, ha, (dec_trivial : (-1 : ℤ) ≠ 1), if_false, ite_eq_left_iff],
+     tauto, }
 
 /-- The quadratic character takes the value `1` on nonzero squares. -/
 lemma quadratic_char_sq_one' {a : F} (ha : a ≠ 0) : quadratic_char F (a ^ 2) = 1 :=
@@ -254,7 +255,7 @@ end
   map_mul' := quadratic_char_mul }
 
 /-- The square of the quadratic character on nonzero arguments is `1`. -/
-lemma quadratic_char_sq_one {a : F} (ha : a ≠ 0) : (quadratic_char F a)^2 = 1 :=
+lemma quadratic_char_sq_one {a : F} (ha : a ≠ 0) : (quadratic_char F a) ^ 2 = 1 :=
 by rwa [pow_two, ← quadratic_char_mul, ← pow_two, quadratic_char_sq_one']
 
 /-- The quadratic character is `1` or `-1` on nonzero arguments. -/

src/number_theory/legendre_symbol/quadratic_reciprocity.lean

@@ -1,16 +1,13 @@
 /-
 Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Chris Hughes
+Authors: Chris Hughes, Michael Stoll
 -/
-
-import field_theory.finite.basic
-import data.zmod.basic
-import data.nat.parity
 import number_theory.legendre_symbol.gauss_eisenstein_lemmas
+import number_theory.legendre_symbol.quadratic_char
 
 /-!
-# Quadratic reciprocity.
+# Legendre symbol and quadratic reciprocity.
 
 This file contains results about quadratic residues modulo a prime number.
 
@@ -32,8 +29,7 @@ Also proven are conditions for `-1` and `2` to be a square modulo a prime,
 The proof of quadratic reciprocity implemented uses Gauss' lemma and Eisenstein's lemma
 -/
 
-open function finset nat finite_field zmod
-open_locale big_operators nat
+open finset nat char
 
 namespace zmod
 
@@ -43,21 +39,15 @@ variables (p q : ℕ) [fact p.prime] [fact q.prime]
 lemma euler_criterion_units (x : (zmod p)ˣ) :
   (∃ y : (zmod p)ˣ, y ^ 2 = x) ↔ x ^ (p / 2) = 1 :=
 begin
-  cases nat.prime.eq_two_or_odd (fact.out p.prime) with hp2 hp_odd,
-  { substI p, refine iff_of_true ⟨1, _⟩ _; apply subsingleton.elim },
-  obtain ⟨g, hg⟩ := is_cyclic.exists_generator (zmod p)ˣ,
-  obtain ⟨n, hn⟩ : x ∈ submonoid.powers g, { rw mem_powers_iff_mem_zpowers, apply hg },
-  split,
-  { rintro ⟨y, rfl⟩, rw [← pow_mul, two_mul_odd_div_two hp_odd, units_pow_card_sub_one_eq_one], },
-  { subst x, assume h,
-    have key : 2 * (p / 2) ∣ n * (p / 2),
-    { rw [← pow_mul] at h,
-      rw [two_mul_odd_div_two hp_odd, ← card_units, ← order_of_eq_card_of_forall_mem_zpowers hg],
-      apply order_of_dvd_of_pow_eq_one h },
-    have : 0 < p / 2 := nat.div_pos (fact.out (1 < p)) dec_trivial,
-    obtain ⟨m, rfl⟩ := dvd_of_mul_dvd_mul_right this key,
-    refine ⟨g ^ m, _⟩,
-    rw [mul_comm, pow_mul], },
+  by_cases hc : p = 2,
+  { substI hc,
+    simp only [eq_iff_true_of_subsingleton, exists_const], },
+  { have h₀ := finite_field.unit_is_square_iff (by rwa ring_char_zmod_n) x,
+    have hs : (∃ y : (zmod p)ˣ, y ^ 2 = x) ↔ is_square(x) :=
+    by { rw is_square_iff_exists_sq x,
+         simp_rw eq_comm, },
+    rw hs,
+    rwa card p at h₀, },
 end
 
 /-- Euler's Criterion: a nonzero `a : zmod p` is a square if and only if `x ^ (p / 2) = 1`. -/
@@ -116,62 +106,101 @@ lemma pow_div_two_eq_neg_one_or_one {a : zmod p} (ha : a ≠ 0) :
   a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1 :=
 begin
   cases nat.prime.eq_two_or_odd (fact.out p.prime) with hp2 hp_odd,
-  { substI p, revert a ha, exact dec_trivial },
+  { substI p, revert a ha, dec_trivial },
   rw [← mul_self_eq_one_iff, ← pow_add, ← two_mul, two_mul_odd_div_two hp_odd],
   exact pow_card_sub_one_eq_one ha
 end
 
-/-- The Legendre symbol of `a` and `p`, `legendre_sym p a`, is an integer defined as
+/-- The Legendre symbol of `a : ℤ` and a prime `p`, `legendre_sym p a`,
+is an integer defined as
 
 * `0` if `a` is `0` modulo `p`;
-* `1` if `a ^ (p / 2)` is `1` modulo `p`
-   (by `euler_criterion` this is equivalent to “`a` is a square modulo `p`”);
+* `1` if `a` is a square modulo `p`
 * `-1` otherwise.
 
 Note the order of the arguments! The advantage of the order chosen here is
 that `legendre_sym p` is a multiplicative function `ℤ → ℤ`.
 -/
-def legendre_sym (p : ℕ) (a : ℤ) : ℤ :=
-if      (a : zmod p) = 0           then  0
-else if (a : zmod p) ^ (p / 2) = 1 then  1
-                                   else -1
+def legendre_sym (p : ℕ) [fact p.prime] (a : ℤ) : ℤ := quadratic_char (zmod p) a
 
+/-- We have the congruence `legendre_sym p a ≡ a ^ (p / 2) mod p`. -/
 lemma legendre_sym_eq_pow (p : ℕ) (a : ℤ) [hp : fact p.prime] :
   (legendre_sym p a : zmod p) = (a ^ (p / 2)) :=
 begin
   rw legendre_sym,
   by_cases ha : (a : zmod p) = 0,
-  { simp only [int.cast_coe_nat, if_pos, ha,
-      zero_pow (nat.div_pos (hp.1.two_le) (succ_pos 1)), int.cast_zero] },
-  cases hp.1.eq_two_or_odd with hp2 hp_odd,
+  { simp only [ha, zero_pow (nat.div_pos (hp.1.two_le) (succ_pos 1)), quadratic_char_zero,
+               int.cast_zero], },
+  by_cases hp₁ : p = 2,
   { substI p,
     generalize : (a : (zmod 2)) = b, revert b, dec_trivial, },
-  { haveI := fact.mk hp_odd,
-    rw [if_neg ha],
-    have : (-1 : zmod p) ≠ 1, from (ne_neg_self p one_ne_zero).symm,
+  { have h₁ := quadratic_char_eq_pow_of_char_ne_two (by rwa ring_char_zmod_n p) ha,
+    rw card p at h₁,
+    rw h₁,
+    have h₂ := finite_field.neg_one_ne_one_of_char_ne_two (by rwa ring_char_zmod_n p),
     cases pow_div_two_eq_neg_one_or_one p ha with h h,
     { rw [if_pos h, h, int.cast_one], },
-    { rw [h, if_neg this, int.cast_neg, int.cast_one], } }
+    { rw [h, if_neg h₂, int.cast_neg, int.cast_one], } }
 end
 
-lemma legendre_sym_eq_one_or_neg_one (p : ℕ) (a : ℤ) (ha : (a : zmod p) ≠ 0) :
-  legendre_sym p a = -1 ∨ legendre_sym p a = 1 :=
+/-- If `p ∤ a`, then `legendre_sym p a` is `1` or `-1`. -/
+lemma legendre_sym_eq_one_or_neg_one (p : ℕ) [fact p.prime] (a : ℤ) (ha : (a : zmod p) ≠ 0) :
+  legendre_sym p a = 1 ∨ legendre_sym p a = -1 :=
+quadratic_char_dichotomy ha
+
+/-- The Legendre symbol of `p` and `a` is zero iff `p ∣ a`. -/
+lemma legendre_sym_eq_zero_iff (p : ℕ) [fact p.prime] (a : ℤ) :
+  legendre_sym p a = 0 ↔ (a : zmod p) = 0 :=
+quadratic_char_eq_zero_iff a
+
+@[simp] lemma legendre_sym_zero (p : ℕ) [fact p.prime] : legendre_sym p 0 = 0 :=
 begin
-  unfold legendre_sym,
-  split_ifs;
-  simp only [*, eq_self_iff_true, or_true, true_or] at *,
+  rw legendre_sym,
+  exact quadratic_char_zero,
 end
 
-lemma legendre_sym_eq_zero_iff (p : ℕ) (a : ℤ) :
-  legendre_sym p a = 0 ↔ (a : zmod p) = 0 :=
+@[simp] lemma legendre_sym_one (p : ℕ) [fact p.prime] : legendre_sym p 1 = 1 :=
+begin
+  rw [legendre_sym, (by norm_cast : ((1 : ℤ) : zmod p) = 1)],
+  exact quadratic_char_one,
+end
+
+/-- The Legendre symbol is multiplicative in `a` for `p` fixed. -/
+lemma legendre_sym_mul (p : ℕ) [fact p.prime] (a b : ℤ) :
+  legendre_sym p (a * b) = legendre_sym p a * legendre_sym p b :=
 begin
-  split,
-  { classical, contrapose,
-    assume ha, cases legendre_sym_eq_one_or_neg_one p a ha with h h,
-    all_goals { rw h, norm_num } },
-  { assume ha, rw [legendre_sym, if_pos ha] }
+  rw [legendre_sym, legendre_sym, legendre_sym],
+  push_cast,
+  exact quadratic_char_mul (a : zmod p) b,
 end
 
+/-- The Legendre symbol is a homomorphism of monoids with zero. -/
+@[simps] def legendre_sym_hom (p : ℕ) [fact p.prime] : ℤ →*₀ ℤ :=
+{ to_fun := legendre_sym p,
+  map_zero' := legendre_sym_zero p,
+  map_one' := legendre_sym_one p,
+  map_mul' := legendre_sym_mul p }
+
+/-- The square of the symbol is 1 if `p ∤ a`. -/
+theorem legendre_sym_sq_one (p : ℕ) [fact p.prime] (a : ℤ) (ha : (a : zmod p) ≠ 0) :
+  (legendre_sym p a)^2 = 1 :=
+quadratic_char_sq_one ha
+
+/-- The Legendre symbol of `a^2` at `p` is 1 if `p ∤ a`. -/
+theorem legendre_sym_sq_one'  (p : ℕ) [fact p.prime] (a : ℤ) (ha : (a : zmod p) ≠ 0) :
+  legendre_sym p (a ^ 2) = 1 :=
+begin
+  rw [legendre_sym],
+  push_cast,
+  exact quadratic_char_sq_one' ha,
+end
+
+/-- The Legendre symbol depends only on `a` mod `p`. -/
+theorem legendre_sym_mod (p : ℕ) [fact p.prime] (a : ℤ) :
+  legendre_sym p a = legendre_sym p (a % p) :=
+by simp only [legendre_sym, int_cast_mod]
+
+
 /-- 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 {a : ℤ} (hp : p ≠ 2) (ha0 : (a : zmod p) ≠ 0) :
@@ -188,14 +217,12 @@ begin
   simp [*, ne_neg_self p one_ne_zero, (ne_neg_self p one_ne_zero).symm] at *
 end
 
+/-- When `p ∤ a`, then `legendre_sym p a = 1` iff `a` is a square mod `p`. -/
 lemma legendre_sym_eq_one_iff {a : ℤ} (ha0 : (a : zmod p) ≠ 0) :
-  legendre_sym p a = 1 ↔ (∃ b : zmod p, b ^ 2 = a) :=
-begin
-  rw [euler_criterion p ha0, legendre_sym, if_neg ha0],
-  split_ifs,
-  { simp only [h, eq_self_iff_true] },
-  { simp only [h, iff_false], tauto }
-end
+  legendre_sym p a = 1 ↔ is_square (a : zmod p) :=
+quadratic_char_one_iff_is_square ha0
+
+open_locale big_operators
 
 lemma eisenstein_lemma (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 :=
@@ -252,12 +279,12 @@ begin
 end
 
 lemma exists_sq_eq_two_iff (hp1 : p ≠ 2) :
-  (∃ a : zmod p, a ^ 2 = 2) ↔ p % 8 = 1 ∨ p % 8 = 7 :=
-have hp2 : ((2 : ℤ) : zmod p) ≠ 0,
-  from prime_ne_zero p 2 (λ h, by simpa [h] using hp1),
-have hpm4 : p % 4 = p % 8 % 4, from (nat.mod_mul_left_mod p 2 4).symm,
-have hpm2 : p % 2 = p % 8 % 2, from (nat.mod_mul_left_mod p 4 2).symm,
+  is_square (2 : zmod p) ↔ p % 8 = 1 ∨ p % 8 = 7 :=
 begin
+  have hp2 : ((2 : ℤ) : zmod p) ≠ 0,
+    from prime_ne_zero p 2 (λ h, by simpa [h] using hp1),
+  have hpm4 : p % 4 = p % 8 % 4, from (nat.mod_mul_left_mod p 2 4).symm,
+  have hpm2 : p % 2 = p % 8 % 2, from (nat.mod_mul_left_mod p 4 2).symm,
   rw [show (2 : zmod p) = (2 : ℤ), by simp, ← legendre_sym_eq_one_iff p hp2],
   erw [legendre_sym_two p hp1, neg_one_pow_eq_one_iff_even (show (-1 : ℤ) ≠ 1, from dec_trivial),
     even_add, even_div, even_div],
@@ -270,39 +297,49 @@ begin
 end
 
 lemma exists_sq_eq_prime_iff_of_mod_four_eq_one (hp1 : p % 4 = 1) (hq1 : q ≠ 2) :
-  (∃ a : zmod p, a ^ 2 = q) ↔ ∃ b : zmod q, b ^ 2 = p :=
+  is_square (q : zmod p) ↔ is_square (p : zmod q) :=
 if hpq : p = q then by substI hpq else
 have h1 : ((p / 2) * (q / 2)) % 2 = 0,
   from (dvd_iff_mod_eq_zero _ _).1
     (dvd_mul_of_dvd_left ((dvd_iff_mod_eq_zero _ _).2 $
     by rw [← mod_mul_right_div_self, show 2 * 2 = 4, from rfl, hp1]; refl) _),
 begin
   have hp_odd : p ≠ 2 := by { by_contra, simp [h] at hp1, norm_num at hp1, },
-  have hpq0 : (p : zmod q) ≠ 0 := prime_ne_zero q p (ne.symm hpq),
-  have hqp0 : (q : zmod p) ≠ 0 := prime_ne_zero p q hpq,
+  have hpq0 : ((p : ℤ) : zmod q) ≠ 0 := prime_ne_zero q p (ne.symm hpq),
+  have hqp0 : ((q : ℤ) : zmod p) ≠ 0 := prime_ne_zero p q hpq,
   have := quadratic_reciprocity p q hp_odd hq1 hpq,
-  rw [neg_one_pow_eq_pow_mod_two, h1, legendre_sym, legendre_sym, int.cast_coe_nat,
-    int.cast_coe_nat, if_neg hqp0, if_neg hpq0] at this,
-  rw [euler_criterion q hpq0, euler_criterion p hqp0],
-  split_ifs at this; simp *; contradiction,
+  rw [neg_one_pow_eq_pow_mod_two, h1, pow_zero] at this,
+  rw [(by norm_cast : (p : zmod q) = (p : ℤ)), (by norm_cast : (q : zmod p) = (q : ℤ)),
+       ← legendre_sym_eq_one_iff _ hpq0, ← legendre_sym_eq_one_iff _ hqp0],
+  cases (legendre_sym_eq_one_or_neg_one p q hqp0) with h h,
+  { simp only [h, eq_self_iff_true, true_iff, mul_one] at this ⊢,
+    exact this, },
+  { simp only [h, mul_neg, mul_one] at this ⊢,
+    rw eq_neg_of_eq_neg this.symm, },
 end
 
 lemma exists_sq_eq_prime_iff_of_mod_four_eq_three (hp3 : p % 4 = 3)
-  (hq3 : q % 4 = 3) (hpq : p ≠ q) : (∃ a : zmod p, a ^ 2 = q) ↔ ¬∃ b : zmod q, b ^ 2 = p :=
+  (hq3 : q % 4 = 3) (hpq : p ≠ q) : is_square (q : zmod p) ↔ ¬ is_square (p : zmod q) :=
 have h1 : ((p / 2) * (q / 2)) % 2 = 1,
   from nat.odd_mul_odd
     (by rw [← mod_mul_right_div_self, show 2 * 2 = 4, from rfl, hp3]; refl)
     (by rw [← mod_mul_right_div_self, show 2 * 2 = 4, from rfl, hq3]; refl),
 begin
   have hp_odd : p ≠ 2 := by { by_contra, simp [h] at hp3, norm_num at hp3, },
   have hq_odd : q ≠ 2 := by { by_contra, simp [h] at hq3, norm_num at hq3, },
-  have hpq0 : (p : zmod q) ≠ 0 := prime_ne_zero q p (ne.symm hpq),
-  have hqp0 : (q : zmod p) ≠ 0 := prime_ne_zero p q hpq,
+  have hpq0 : ((p : ℤ) : zmod q) ≠ 0 := prime_ne_zero q p (ne.symm hpq),
+  have hqp0 : ((q : ℤ) : zmod p) ≠ 0 := prime_ne_zero p q hpq,
   have := quadratic_reciprocity p q hp_odd hq_odd hpq,
-  rw [neg_one_pow_eq_pow_mod_two, h1, legendre_sym, legendre_sym, int.cast_coe_nat,
-    int.cast_coe_nat, if_neg hpq0, if_neg hqp0] at this,
-  rw [euler_criterion q hpq0, euler_criterion p hqp0],
-  split_ifs at this; simp *; contradiction
+  rw [neg_one_pow_eq_pow_mod_two, h1, pow_one] at this,
+  rw [(by norm_cast : (p : zmod q) = (p : ℤ)), (by norm_cast : (q : zmod p) = (q : ℤ)),
+       ← legendre_sym_eq_one_iff _ hpq0, ← legendre_sym_eq_one_iff _ hqp0],
+  cases (legendre_sym_eq_one_or_neg_one q p hpq0) with h h,
+  { simp only [h, eq_self_iff_true, not_true, iff_false, one_mul] at this ⊢,
+    simp only [this],
+    norm_num, },
+  { simp only [h, neg_mul, one_mul, neg_inj] at this ⊢,
+    simp only [this, eq_self_iff_true, true_iff],
+    norm_num, },
 end
 
 end zmod