feat(number_theory/legendre_symbol/): add some lemmas (#13831)

This adds essentially two lemmas on quadratic characters:
* `quadratic_char_neg_one_iff_not_is_square`, which says that the quadratic character takes the value `-1` exactly on non-squares, and
* `quadratic_char_number_of_sqrts`. which says that the number of square roots of `a : F` is `quadratic_char F a + 1`.

It also adds the corresponding statements, `legendre_sym_eq_neg_one_iff` and `legendre_sym_number_of_sqrts`, for the Legendre symbol.

src/number_theory/legendre_symbol/quadratic_char.lean

@@ -58,6 +58,16 @@ begin
   exact char_p.neg_one_ne_one _ (ring_char F),
 end
 
+/-- Characteristic `≠ 2` implies that `-a ≠ a` when `a ≠ 0`. -/
+lemma neg_ne_self_of_char_ne_two (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) : a ≠ -a :=
+begin
+  intro hf,
+  rw [eq_neg_iff_add_eq_zero, (by ring : a + a = 2 * a), mul_eq_zero] at hf,
+  have h := mt eq_neg_iff_add_eq_zero.mpr (neg_one_ne_one_of_char_ne_two hF).symm,
+  norm_num at h,
+  exact or.dcases_on hf (λ (hf : 2 = 0), h hf) (λ (hf : a = 0), ha hf),
+end
+
 /-- If `F` has odd characteristic, then for nonzero `a : F`, we have that `a ^ (#F / 2) = ±1`. -/
 lemma pow_dichotomy (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) :
   a^(fintype.card F / 2) = 1 ∨ a^(fintype.card F / 2) = -1 :=
@@ -263,14 +273,69 @@ lemma quadratic_char_dichotomy {a : F} (ha : a ≠ 0) :
   quadratic_char F a = 1 ∨ quadratic_char F a = -1 :=
 (sq_eq_one_iff (quadratic_char F a)).mp (quadratic_char_sq_one ha)
 
+/-- A variant -/
+lemma quadratic_char_eq_neg_one_iff_not_one {a : F} (ha : a ≠ 0) :
+  quadratic_char F a = -1 ↔ ¬ quadratic_char F a = 1 :=
+begin
+  split,
+  { intro h,
+    rw h,
+    norm_num, },
+  { exact λ h₂, (or_iff_right h₂).mp (quadratic_char_dichotomy ha), }
+end
+
+/-- For `a : F`, `quadratic_char F a = -1 ↔ ¬ is_square a`. -/
+lemma quadratic_char_neg_one_iff_not_is_square {a : F} :
+  quadratic_char F a = -1 ↔ ¬ is_square a :=
+begin
+  by_cases ha : a = 0,
+  { simp only [ha, is_square_zero, quadratic_char_zero, zero_eq_neg, one_ne_zero, not_true], },
+  { rw quadratic_char_eq_neg_one_iff_not_one ha,
+    exact not_iff_not.mpr (quadratic_char_one_iff_is_square ha), },
+end
+
 /-- If `F` has odd characteristic, then `quadratic_char F` takes the value `-1`. -/
 lemma quadratic_char_exists_neg_one (hF : ring_char F ≠ 2) : ∃ a, quadratic_char F a = -1 :=
+Exists.dcases_on (finite_field.exists_nonsquare hF)
+  (λ (b : F) (h₁ : ¬is_square b), ⟨b, (quadratic_char_neg_one_iff_not_is_square.mpr h₁)⟩)
+
+/-- The number of solutions to `x^2 = a` is determined by the quadratic character. -/
+lemma quadratic_char_card_sqrts (hF : ring_char F ≠ 2) (a : F) :
+  ↑{x : F | x^2 = a}.to_finset.card = quadratic_char F a + 1 :=
 begin
-  cases (finite_field.exists_nonsquare hF) with b h₁,
-  have hb : b ≠ 0 := by { intro hf, rw hf at h₁, exact h₁ (is_square_zero F), },
-  use b,
-  simp only [quadratic_char, hb, if_false, ite_eq_right_iff],
-  tauto,
+  -- we consider the cases `a = 0`, `a` is a nonzero square and `a` is a nonsquare in turn
+  by_cases h₀ : a = 0,
+  { simp only [h₀, pow_eq_zero_iff, nat.succ_pos', int.coe_nat_succ, int.coe_nat_zero, zero_add,
+               quadratic_char_zero, add_zero, set.set_of_eq_eq_singleton, set.to_finset_card,
+               set.card_singleton], },
+  { set s := {x : F | x^2 = a}.to_finset with hs,
+    by_cases h : is_square a,
+    { rw (quadratic_char_one_iff_is_square h₀).mpr h,
+      rcases h with ⟨b, h⟩,
+      have hb₀ : b ≠ 0 := by { intro hb, rw [hb, mul_zero] at h, exact h₀ h, },
+      have h₁ : s = [b, -b].to_finset := by
+      { ext x,
+        simp only [finset.mem_filter, finset.mem_univ, true_and, list.to_finset_cons,
+                   list.to_finset_nil, insert_emptyc_eq, finset.mem_insert, finset.mem_singleton],
+        rw ← pow_two at h,
+        rw hs,
+        simp only [set.mem_to_finset, set.mem_set_of_eq],
+        rw h,
+        split,
+        { exact eq_or_eq_neg_of_sq_eq_sq _ _, },
+        { rintro (h₂ | h₂); rw h₂,
+          simp only [neg_sq], }, },
+      simp only [h₁, finset.card_doubleton (finite_field.neg_ne_self_of_char_ne_two hF hb₀),
+                 list.to_finset_cons, list.to_finset_nil, insert_emptyc_eq, int.coe_nat_succ,
+                 int.coe_nat_zero, zero_add], },
+    { rw quadratic_char_neg_one_iff_not_is_square.mpr h,
+      simp only [int.coe_nat_eq_zero, finset.card_eq_zero, set.to_finset_card,
+                 fintype.card_of_finset, set.mem_set_of_eq, add_left_neg],
+      ext x,
+      simp only [iff_false, finset.mem_filter, finset.mem_univ, true_and, finset.not_mem_empty],
+      rw is_square_iff_exists_sq at h,
+      push_neg at h,
+      exact (h x).symm, }, },
 end
 
 open_locale big_operators

src/number_theory/legendre_symbol/quadratic_reciprocity.lean

@@ -62,6 +62,7 @@ begin
     refine ⟨units.mk0 y hy, _⟩, simp, }
 end
 
+-- The following is used by number_theory/zsqrtd/gaussian_int.lean and archive/imo/imo2008_q3.lean
 lemma exists_sq_eq_neg_one_iff :
   (∃ y : zmod p, y ^ 2 = -1) ↔ p % 4 ≠ 3 :=
 begin
@@ -148,6 +149,10 @@ lemma legendre_sym_eq_one_or_neg_one (p : ℕ) [fact p.prime] (a : ℤ) (ha : (a
   legendre_sym p a = 1 ∨ legendre_sym p a = -1 :=
 quadratic_char_dichotomy ha
 
+lemma legendre_sym_eq_neg_one_iff_not_one {a : ℤ} (ha : (a : zmod p) ≠ 0) :
+  legendre_sym p a = -1 ↔ ¬ legendre_sym p a = 1 :=
+quadratic_char_eq_neg_one_iff_not_one 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 :=
@@ -222,6 +227,19 @@ lemma legendre_sym_eq_one_iff {a : ℤ} (ha0 : (a : zmod p) ≠ 0) :
   legendre_sym p a = 1 ↔ is_square (a : zmod p) :=
 quadratic_char_one_iff_is_square ha0
 
+/-- `legendre_sym p a = -1` iff`a` is a nonsquare mod `p`. -/
+lemma legendre_sym_eq_neg_one_iff {a : ℤ} :
+  legendre_sym p a = -1 ↔ ¬ is_square (a : zmod p) :=
+quadratic_char_neg_one_iff_not_is_square
+
+/-- The number of square roots of `a` modulo `p` is determined by the Legendre symbol. -/
+lemma legendre_sym_card_sqrts (hp : p ≠ 2) (a : ℤ) :
+  ↑{x : zmod p | x^2 = a}.to_finset.card = legendre_sym p a + 1 :=
+begin
+  have h : ring_char (zmod p) ≠ 2 := by { rw ring_char_zmod_n, exact hp, },
+  exact quadratic_char_card_sqrts h a,
+end
+
 open_locale big_operators
 
 lemma eisenstein_lemma (hp : p ≠ 2) {a : ℕ} (ha1 : a % 2 = 1) (ha0 : (a : zmod p) ≠ 0) :