[Merged by Bors] - feat(number_theory/legendre_symbol/*): add results on value at -1

archive/imo/imo2008_q3.lean

@@ -43,7 +43,7 @@ begin
     simp only [int.nat_abs_sq, int.coe_nat_pow, int.coe_nat_succ, int.coe_nat_dvd.mp],
     refine (zmod.int_coe_zmod_eq_zero_iff_dvd (m ^ 2 + 1) p).mp _,
     simp only [int.cast_pow, int.cast_add, int.cast_one, zmod.coe_val_min_abs],
-    rw hy, exact add_left_neg 1 },
+    rw [pow_two, ← hy], exact add_left_neg 1 },
 
   have hnat₂ : n ≤ p / 2 := zmod.nat_abs_val_min_abs_le y,
   have hnat₃ : p ≥ 2 * n, { linarith [nat.div_mul_le_self p 2] },

src/number_theory/legendre_symbol/quadratic_char.lean

@@ -5,6 +5,7 @@ Authors: Michael Stoll
 -/
 import tactic.basic
 import field_theory.finite.basic
+import data.int.range
 
 /-!
 # Quadratic characters of finite fields
@@ -18,11 +19,28 @@ quadratic character
 -/
 
 /-!
-### Some general results on finite fields
+### Some general results, mostly on finite fields
+
+We collect some results here that are not specific to quadratic characters
+but are needed below. They will be moved to appropriate places eventually.
 -/
 
 section general
 
+/-- A natural number is odd iff it has residue `1` or `3` mod `4`-/
+lemma nat.odd_mod_four_iff {n : ℕ} : n % 2 = 1 ↔ n % 4 = 1 ∨ n % 4 = 3 :=
+begin
+  split,
+  { have help : ∀ (m : ℕ), 0 ≤ m → m < 4 → m % 2 = 1 → m = 1 ∨ m = 3 := dec_trivial,
+    intro hn,
+    rw [← nat.mod_mod_of_dvd n (by norm_num : 2 ∣ 4)] at hn,
+    exact help (n % 4) zero_le' (nat.mod_lt n (by norm_num)) hn, },
+  { intro h,
+    cases h with h h,
+    { exact nat.odd_of_mod_four_eq_one h, },
+    { exact nat.odd_of_mod_four_eq_three h }, },
+end
+
 /-- If `ring_char R = 2`, where `R` is a finite reduced commutative ring,
 then every `a : R` is a square. -/
 lemma is_square_of_char_two' {R : Type*} [fintype R] [comm_ring R] [is_reduced R] [char_p R 2]
@@ -41,15 +59,29 @@ begin
   exact is_square_of_char_two' a,
 end
 
-/-- If the finite field `F` has characteristic `≠ 2`, then it has odd cardinatlity. -/
-lemma odd_card_of_char_ne_two (hF : ring_char F ≠ 2) : fintype.card F % 2 = 1 :=
+/-- The finite field `F` has even cardinality iff it has characteristic `2`. -/
+lemma even_card_iff_char_two : ring_char F = 2 ↔ fintype.card F % 2 = 0 :=
 begin
-  rcases finite_field.card F (ring_char F) with ⟨ n, hp, h ⟩,
-  have h₁ : odd ((ring_char F) ^ (n : ℕ)) :=
-    odd.pow ((or_iff_right hF).mp (nat.prime.eq_two_or_odd' hp)),
-  rwa [← h, nat.odd_iff] at h₁,
+  rcases finite_field.card F (ring_char F) with ⟨n, hp, h⟩,
+  rw [h, nat.pow_mod],
+  split,
+  { intro hF,
+    rw hF,
+    simp only [nat.bit0_mod_two, zero_pow', ne.def, pnat.ne_zero, not_false_iff, nat.zero_mod], },
+  { rw [← nat.even_iff, nat.even_pow],
+    rintros ⟨hev, hnz⟩,
+    rw [nat.even_iff, nat.mod_mod] at hev,
+    cases (nat.prime.eq_two_or_odd hp) with h₁ h₁,
+    { exact h₁, },
+    { exact false.rec (ring_char F = 2) (one_ne_zero ((eq.symm h₁).trans hev)), }, },
 end
 
+lemma even_card_of_char_two (hF : ring_char F = 2) : fintype.card F % 2 = 0 :=
+even_card_iff_char_two.mp hF
+
+lemma odd_card_of_char_ne_two (hF : ring_char F ≠ 2) : fintype.card F % 2 = 1 :=
+nat.mod_two_ne_zero.mp (mt even_card_iff_char_two.mpr hF)
+
 /-- Characteristic `≠ 2` implies that `-1 ≠ 1`. -/
 lemma neg_one_ne_one_of_char_ne_two (hF : ring_char F ≠ 2) : (-1 : F) ≠ 1 :=
 begin
@@ -365,10 +397,45 @@ section quad_char_mod_p
 
 /-- Define the nontrivial quadratic character on `zmod 4`, `χ₄`.
 It corresponds to the extension `ℚ(√-1)/ℚ`. -/
-
 @[simps] def χ₄ : (zmod 4) →*₀ ℤ :=
 { to_fun := (![0,1,0,-1] : (zmod 4 → ℤ)),
-  map_zero' := rfl, map_one' := rfl, map_mul' := by dec_trivial }
+  map_zero' := rfl, map_one' := rfl, map_mul' := dec_trivial }
+
+/-- An explicit description of `χ₄` on integers / naturals -/
+lemma χ₄_int_eq_if_mod_four (n : ℤ) : χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 :=
+begin
+  have help : ∀ (m : ℤ), 0 ≤ m → m < 4 → χ₄ m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1 :=
+  dec_trivial,
+  rw [← int.mod_mod_of_dvd n (by norm_num : (2 : ℤ) ∣ 4), ← zmod.int_cast_mod n 4],
+  exact help (n % 4) (int.mod_nonneg n (by norm_num)) (int.mod_lt n (by norm_num)),
+end
+
+lemma χ₄_nat_eq_if_mod_four (n : ℕ) : χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 :=
+by exact_mod_cast χ₄_int_eq_if_mod_four n
+
+/-- Alternative description for odd `n : ℕ` in terms of powers of `-1` -/
+lemma χ₄_eq_neg_one_pow {n : ℕ} (hn : n % 2 = 1) : χ₄ n = (-1)^(n / 2) :=
+begin
+  rw χ₄_nat_eq_if_mod_four,
+  simp only [hn, nat.one_ne_zero, if_false],
+  have h := (nat.div_add_mod n 4).symm,
+  cases (nat.odd_mod_four_iff.mp hn) with h4 h4,
+  { split_ifs,
+    rw h4 at h,
+    rw [h],
+    nth_rewrite 0 (by norm_num : 4 = 2 * 2),
+    rw [mul_assoc, add_comm, nat.add_mul_div_left _ _ (by norm_num : 0 < 2), pow_add, pow_mul],
+    norm_num, },
+  { split_ifs,
+    { exfalso,
+      rw h4 at h_1,
+      norm_num at h_1, },
+    { rw h4 at h,
+      rw [h],
+      nth_rewrite 0 (by norm_num : 4 = 2 * 2),
+      rw [mul_assoc, add_comm, nat.add_mul_div_left _ _ (by norm_num : 0 < 2), pow_add, pow_mul],
+      norm_num, }, },
+end
 
 /-- Define the first primitive quadratic character on `zmod 8`, `χ₈`.
 It corresponds to the extension `ℚ(√2)/ℚ`. -/
@@ -385,3 +452,58 @@ It corresponds to the extension `ℚ(√-2)/ℚ`. -/
 end quad_char_mod_p
 
 end zmod
+
+/-!
+### Special values of the quadratic character
+
+We express `quadratic_char F (-1)` in terms of `χ₄`.
+-/
+
+section special_values
+
+namespace char
+
+open zmod
+
+variables {F : Type*} [field F] [fintype F]
+
+/-- The value of the quadratic character at `-1` -/
+lemma quadratic_char_neg_one [decidable_eq F] (hF : ring_char F ≠ 2) :
+  quadratic_char F (-1) = χ₄ (fintype.card F) :=
+begin
+  have h₁ : (-1 : F) ≠ 0 := by { rw neg_ne_zero, exact one_ne_zero },
+  have h := quadratic_char_eq_pow_of_char_ne_two hF h₁,
+  rw [h, χ₄_eq_neg_one_pow (finite_field.odd_card_of_char_ne_two hF)],
+  set n := fintype.card F / 2,
+  cases (nat.even_or_odd n) with h₂ h₂,
+  { simp only [even.neg_one_pow h₂, eq_self_iff_true, if_true], },
+  { simp only [odd.neg_one_pow h₂, ite_eq_right_iff],
+    exact λ (hf : -1 = 1),
+            false.rec (1 = -1) (finite_field.neg_one_ne_one_of_char_ne_two hF hf), },
+end
+
+/-- The interpretation in terms of whether `-1` is a square in `F` -/
+lemma is_square_neg_one_iff : is_square (-1 : F) ↔ fintype.card F % 4 ≠ 3 :=
+begin
+  classical, -- suggested by the linter (instead of `[decidable_eq F]`)
+  by_cases hF : (ring_char F = 2),
+  { simp only [finite_field.is_square_of_char_two hF, ne.def, true_iff],
+    exact (λ hf, one_ne_zero ((nat.odd_of_mod_four_eq_three hf).symm.trans
+                                (finite_field.even_card_of_char_two hF)))},
+  { have h₁ : (-1 : F) ≠ 0 := by { rw neg_ne_zero, exact one_ne_zero },
+    have h₂ := finite_field.odd_card_of_char_ne_two hF,
+    rw [← quadratic_char_one_iff_is_square h₁, quadratic_char_neg_one hF,
+        χ₄_nat_eq_if_mod_four, h₂],
+    have h₃ := nat.odd_mod_four_iff.mp h₂,
+    simp only [nat.one_ne_zero, if_false, ite_eq_left_iff, ne.def],
+    norm_num,
+    split,
+    { intros h h',
+      have t := (of_not_not h).symm.trans h',
+      norm_num at t, },
+    exact λ h h', h' ((or_iff_left h).mp h₃), },
+end
+
+end char
+
+end special_values

src/number_theory/legendre_symbol/quadratic_reciprocity.lean

@@ -21,8 +21,8 @@ interpretations in terms of existence of square roots depending on the congruenc
 `exists_sq_eq_prime_iff_of_mod_four_eq_three`.
 
 Also proven are conditions for `-1` and `2` to be a square modulo a prime,
-`exists_sq_eq_neg_one_iff` and
-`exists_sq_eq_two_iff`
+`legende_sym_neg_one` and `exists_sq_eq_neg_one_iff` for `-1`, and
+`exists_sq_eq_two_iff` for `2`
 
 ## Implementation notes
 
@@ -52,41 +52,28 @@ end
 
 /-- Euler's Criterion: a nonzero `a : zmod p` is a square if and only if `x ^ (p / 2) = 1`. -/
 lemma euler_criterion {a : zmod p} (ha : a ≠ 0) :
-  (∃ y : zmod p, y ^ 2 = a) ↔ a ^ (p / 2) = 1 :=
+  is_square (a : zmod p) ↔ a ^ (p / 2) = 1 :=
 begin
   apply (iff_congr _ (by simp [units.ext_iff])).mp (euler_criterion_units p (units.mk0 a ha)),
   simp only [units.ext_iff, sq, units.coe_mk0, units.coe_mul],
-  split, { rintro ⟨y, hy⟩, exact ⟨y, hy⟩ },
+  split, { rintro ⟨y, hy⟩, exact ⟨y, hy.symm⟩ },
   { rintro ⟨y, rfl⟩,
     have hy : y ≠ 0, { rintro rfl, simpa [zero_pow] using ha, },
     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 :=
+lemma exists_sq_eq_neg_one_iff : is_square (-1 : zmod p) ↔ p % 4 ≠ 3 :=
 begin
-  cases nat.prime.eq_two_or_odd (fact.out p.prime) with hp2 hp_odd,
-  { substI p, exact dec_trivial },
-  haveI := fact.mk hp_odd,
-  have neg_one_ne_zero : (-1 : zmod p) ≠ 0, from mt neg_eq_zero.1 one_ne_zero,
-  rw [euler_criterion p neg_one_ne_zero, neg_one_pow_eq_pow_mod_two],
-  cases mod_two_eq_zero_or_one (p / 2) with p_half_even p_half_odd,
-  { rw [p_half_even, pow_zero, eq_self_iff_true, true_iff],
-    contrapose! p_half_even with hp,
-    rw [← nat.mod_mul_right_div_self, show 2 * 2 = 4, from rfl, hp],
-    exact dec_trivial },
-  { rw [p_half_odd, pow_one,
-        iff_false_intro (ne_neg_self p one_ne_zero).symm, false_iff, not_not],
-    rw [← nat.mod_mul_right_div_self, show 2 * 2 = 4, from rfl] at p_half_odd,
-    rw [← nat.mod_mul_left_mod _ 2, show 2 * 2 = 4, from rfl] at hp_odd,
-    have hp : p % 4 < 4, from nat.mod_lt _ dec_trivial,
-    revert hp hp_odd p_half_odd,
-    generalize : p % 4 = k, dec_trivial! }
+  have h := @is_square_neg_one_iff (zmod p) _ _,
+  rw card p at h,
+  exact h,
 end
 
 lemma mod_four_ne_three_of_sq_eq_neg_one {y : zmod p} (hy : y ^ 2 = -1) : p % 4 ≠ 3 :=
-(exists_sq_eq_neg_one_iff p).1 ⟨y, hy⟩
+begin
+  rw pow_two at hy,
+  exact (exists_sq_eq_neg_one_iff p).1 ⟨y, hy.symm⟩
+end
 
 lemma mod_four_ne_three_of_sq_eq_neg_sq' {x y : zmod p} (hy : y ≠ 0) (hxy : x ^ 2 = - y ^ 2) :
   p % 4 ≠ 3 :=
@@ -240,6 +227,15 @@ begin
   exact quadratic_char_card_sqrts h a,
 end
 
+/-- `legendre_sym p (-1)` is given by `χ₄ p`. -/
+lemma legendre_sym_neg_one (hp : p ≠ 2) : legendre_sym p (-1) = χ₄ p :=
+begin
+  have h : ring_char (zmod p) ≠ 2 := by { rw ring_char_zmod_n, exact hp, },
+  have h₁ := quadratic_char_neg_one h,
+  rw card p at h₁,
+  exact_mod_cast h₁,
+end
+
 open_locale big_operators
 
 lemma eisenstein_lemma (hp : p ≠ 2) {a : ℕ} (ha1 : a % 2 = 1) (ha0 : (a : zmod p) ≠ 0) :

src/number_theory/zsqrtd/gaussian_int.lean

@@ -211,7 +211,8 @@ hp.1.eq_two_or_odd.elim
       obtain ⟨k, k_lt_p, rfl⟩ : ∃ (k' : ℕ) (h : k' < p), (k' : zmod p) = k,
       { refine ⟨k.val, k.val_lt, zmod.nat_cast_zmod_val k⟩ },
       have hpk : p ∣ k ^ 2 + 1,
-        by rw [← char_p.cast_eq_zero_iff (zmod p) p]; simp *,
+        by { rw [pow_two, ← char_p.cast_eq_zero_iff (zmod p) p, nat.cast_add, nat.cast_mul,
+                 nat.cast_one, ← hk, add_left_neg], },
       have hkmul : (k ^ 2 + 1 : ℤ[i]) = ⟨k, 1⟩ * ⟨k, -1⟩ :=
         by simp [sq, zsqrtd.ext],
       have hpne1 : p ≠ 1 := ne_of_gt hp.1.one_lt,