feat(number_theory/legendre_symbol/quadratic_reciprocity): Alternate …

…forms of `exists_sq_eq_neg_one` (#13594)

Also, renamed `exists_sq_eq_neg_one_iff_mod_four_ne_three` to `exists_sq_eq_neg_one` for consistency with `exists_sq_eq_two` and for convenience.

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_mod_four_ne_three p).mpr hp_mod_4_ne_3,
+  obtain ⟨y, hy⟩ := (zmod.exists_sq_eq_neg_one_iff p).mpr hp_mod_4_ne_3,
 
   let m := zmod.val_min_abs y,
   let n := int.nat_abs m,

src/number_theory/legendre_symbol/quadratic_reciprocity.lean

@@ -24,7 +24,7 @@ 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_mod_four_ne_three` and
+`exists_sq_eq_neg_one_iff` and
 `exists_sq_eq_two_iff`
 
 ## Implementation notes
@@ -72,7 +72,7 @@ begin
     refine ⟨units.mk0 y hy, _⟩, simp, }
 end
 
-lemma exists_sq_eq_neg_one_iff_mod_four_ne_three :
+lemma exists_sq_eq_neg_one_iff :
   (∃ y : zmod p, y ^ 2 = -1) ↔ p % 4 ≠ 3 :=
 begin
   cases nat.prime.eq_two_or_odd (fact.out p.prime) with hp2 hp_odd,
@@ -94,6 +94,24 @@ begin
     generalize : p % 4 = k, dec_trivial! }
 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⟩
+
+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 :=
+@mod_four_ne_three_of_sq_eq_neg_one p _ (x / y) begin
+  apply_fun (λ z, z / y ^ 2) at hxy,
+  rwa [neg_div, ←div_pow, ←div_pow, div_self hy, one_pow] at hxy
+end
+
+lemma mod_four_ne_three_of_sq_eq_neg_sq {x y : zmod p} (hx : x ≠ 0) (hxy : x ^ 2 = - y ^ 2) :
+  p % 4 ≠ 3 :=
+begin
+  apply_fun (λ x, -x) at hxy,
+  rw neg_neg at hxy,
+  exact mod_four_ne_three_of_sq_eq_neg_sq' p hx hxy.symm
+end
+
 lemma pow_div_two_eq_neg_one_or_one {a : zmod p} (ha : a ≠ 0) :
   a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1 :=
 begin

src/number_theory/zsqrtd/gaussian_int.lean

@@ -205,7 +205,7 @@ hp.1.eq_two_or_odd.elim
         revert this hp3 hp1,
         generalize : p % 4 = m, dec_trivial!,
       end,
-    let ⟨k, hk⟩ := (zmod.exists_sq_eq_neg_one_iff_mod_four_ne_three p).2 $
+    let ⟨k, hk⟩ := (zmod.exists_sq_eq_neg_one_iff p).2 $
       by rw hp41; exact dec_trivial in
     begin
       obtain ⟨k, k_lt_p, rfl⟩ : ∃ (k' : ℕ) (h : k' < p), (k' : zmod p) = k,