feat(<various>): add a bunch of lemmas for use with Jacobi symbols (#…

…16290)

This PR introduces a number of lemmas that will be needed for proving results about the Jacobi symbol (to be introduced in a follow-up PR). (Originally, the Jacobi symbol results were included here; see the discussion below.)

Discussion on [Zuilp](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Jacobi.20symbol/near/295816984).

src/data/list/basic.lean

@@ -2749,6 +2749,23 @@ begin
     { simpa [hl] } }
 end
 
+lemma pmap_append {p : ι → Prop} (f : Π (a : ι), p a → α) (l₁ l₂ : list ι)
+  (h : ∀ a ∈ l₁ ++ l₂, p a) :
+  (l₁ ++ l₂).pmap f h = l₁.pmap f (λ a ha, h a (mem_append_left l₂ ha)) ++
+                        l₂.pmap f (λ a ha, h a (mem_append_right l₁ ha)) :=
+begin
+  induction l₁ with _ _ ih,
+  { refl, },
+  { dsimp only [pmap, cons_append],
+    rw ih, }
+end
+
+lemma pmap_append' {α β : Type*} {p : α → Prop} (f : Π (a : α), p a → β) (l₁ l₂ : list α)
+  (h₁ : ∀ a ∈ l₁, p a) (h₂ : ∀ a ∈ l₂, p a) :
+  (l₁ ++ l₂).pmap f (λ a ha, (list.mem_append.1 ha).elim (h₁ a) (h₂ a)) =
+  l₁.pmap f h₁ ++ l₂.pmap f h₂ :=
+pmap_append f l₁ l₂ _
+
 /-! ### find -/
 
 section find

src/data/nat/factorization/basic.lean

@@ -482,6 +482,14 @@ begin
   { simp [hqp, (factorization_le_iff_dvd hd0 hn0).2 hdn q] },
 end
 
+/-- If `n` is a nonzero natural number and `p ≠ 1`, then there are natural numbers `e`
+and `n'` such that `n'` is not divisible by `p` and `n = p^e * n'`. -/
+lemma exists_eq_pow_mul_and_not_dvd {n : ℕ} (hn : n ≠ 0) (p : ℕ) (hp : p ≠ 1) :
+  ∃ e n' : ℕ, ¬ p ∣ n' ∧ n = p ^ e * n' :=
+let ⟨a', h₁, h₂⟩ := multiplicity.exists_eq_pow_mul_and_not_dvd
+                      (multiplicity.finite_nat_iff.mpr ⟨hp, nat.pos_of_ne_zero hn⟩) in
+⟨_, a', h₂, h₁⟩
+
 lemma dvd_iff_div_factorization_eq_tsub {d n : ℕ} (hd : d ≠ 0) (hdn : d ≤ n) :
   d ∣ n ↔ (n / d).factorization = n.factorization - d.factorization :=
 begin

src/data/nat/parity.lean

@@ -227,3 +227,25 @@ variables {R : Type*} [monoid R] [has_distrib_neg R] {n : ℕ}
 lemma neg_one_pow_eq_one_iff_even (h : (-1 : R) ≠ 1) : (-1 : R) ^ n = 1 ↔ even n :=
 ⟨λ h', of_not_not $ λ hn, h $ (odd.neg_one_pow $ odd_iff_not_even.mpr hn).symm.trans h',
   even.neg_one_pow⟩
+
+/-- If `a` is even, then `n` is odd iff `n % a` is odd. -/
+lemma odd.mod_even_iff {n a : ℕ} (ha : even a) : odd (n % a) ↔ odd n :=
+((even_sub' $ mod_le n a).mp $ even_iff_two_dvd.mpr $ (even_iff_two_dvd.mp ha).trans $
+   dvd_sub_mod n).symm
+
+/-- If `a` is even, then `n` is even iff `n % a` is even. -/
+lemma even.mod_even_iff {n a : ℕ} (ha : even a) : even (n % a) ↔ even n :=
+((even_sub $ mod_le n a).mp $ even_iff_two_dvd.mpr $ (even_iff_two_dvd.mp ha).trans $
+   dvd_sub_mod n).symm
+
+/-- If `n` is odd and `a` is even, then `n % a` is odd. -/
+lemma odd.mod_even {n a : ℕ} (hn : odd n) (ha : even a) : odd (n % a) :=
+(odd.mod_even_iff ha).mpr hn
+
+/-- If `n` is even and `a` is even, then `n % a` is even. -/
+lemma even.mod_even {n a : ℕ} (hn : even n) (ha : even a) : even (n % a) :=
+(even.mod_even_iff ha).mpr hn
+
+/-- `2` is not a prime factor of an odd natural number. -/
+lemma odd.factors_ne_two {n p : ℕ} (hn : odd n) (hp : p ∈ n.factors) : p ≠ 2 :=
+by { rintro rfl, exact two_dvd_ne_zero.mpr (odd_iff.mp hn) (dvd_of_mem_factors hp) }

src/data/sign.lean

@@ -174,6 +174,13 @@ end cast
   map_one'  := rfl,
   map_mul'  := λ x y, by cases x; cases y; simp }
 
+lemma range_eq {α} (f : sign_type → α) : set.range f = {f zero, f neg, f pos} :=
+begin
+  classical,
+  simpa only [← finset.coe_singleton, ← finset.image_singleton,
+    ← fintype.coe_image_univ, finset.coe_image, ← set.image_insert_eq],
+end
+
 end sign_type
 
 variables {α : Type*}

src/data/zmod/coprime.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2022 Michael Stoll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Stoll
+-/
+import data.zmod.basic
+import ring_theory.int.basic
+
+/-!
+# Coprimality and vanishing
+
+We show that for prime `p`, the image of an integer `a` in `zmod p` vanishes if and only if
+`a` and `p` are not coprime.
+-/
+
+namespace zmod
+
+/-- If `p` is a prime and `a` is an integer, then `a : zmod p` is zero if and only if
+`gcd a p ≠ 1`. -/
+lemma eq_zero_iff_gcd_ne_one {a : ℤ} {p : ℕ} [pp : fact p.prime] : (a : zmod p) = 0 ↔ a.gcd p ≠ 1 :=
+by rw [ne, int.gcd_comm, int.gcd_eq_one_iff_coprime,
+       (nat.prime_iff_prime_int.1 pp.1).coprime_iff_not_dvd, not_not, int_coe_zmod_eq_zero_iff_dvd]
+
+/-- If an integer `a` and a prime `p` satisfy `gcd a p = 1`, then `a : zmod p` is nonzero. -/
+lemma ne_zero_of_gcd_eq_one {a : ℤ} {p : ℕ} (pp : p.prime) (h : a.gcd p = 1) :
+  (a : zmod p) ≠ 0 :=
+mt (@eq_zero_iff_gcd_ne_one a p ⟨pp⟩).mp (not_not.mpr h)
+
+/-- If an integer `a` and a prime `p` satisfy `gcd a p ≠ 1`, then `a : zmod p` is zero. -/
+lemma eq_zero_of_gcd_ne_one {a : ℤ} {p : ℕ} (pp : p.prime) (h : a.gcd p ≠ 1) :
+  (a : zmod p) = 0 :=
+(@eq_zero_iff_gcd_ne_one a p ⟨pp⟩).mpr h
+
+end zmod

src/number_theory/legendre_symbol/zmod_char.lean

@@ -40,6 +40,14 @@ It corresponds to the extension `ℚ(√-1)/ℚ`. -/
 /-- `χ₄` takes values in `{0, 1, -1}` -/
 lemma is_quadratic_χ₄ : χ₄.is_quadratic := by { intro a, dec_trivial!, }
 
+/-- The value of `χ₄ n`, for `n : ℕ`, depends only on `n % 4`. -/
+lemma χ₄_nat_mod_four (n : ℕ) : χ₄ n = χ₄ (n % 4 : ℕ) :=
+by rw ← zmod.nat_cast_mod n 4
+
+/-- The value of `χ₄ n`, for `n : ℤ`, depends only on `n % 4`. -/
+lemma χ₄_int_mod_four (n : ℤ) : χ₄ n = χ₄ (n % 4 : ℤ) :=
+by { rw ← zmod.int_cast_mod n 4, norm_cast, }
+
 /-- 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
@@ -52,7 +60,7 @@ 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` -/
+/-- Alternative description of `χ₄ n` 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,
@@ -67,6 +75,22 @@ begin
     ((nat.mod_mod_of_dvd n (by norm_num : 2 ∣ 4)).trans hn),
 end
 
+/-- If `n % 4 = 1`, then `χ₄ n = 1`. -/
+lemma χ₄_nat_one_mod_four {n : ℕ} (hn : n % 4 = 1) : χ₄ n = 1 :=
+by { rw [χ₄_nat_mod_four, hn], refl }
+
+/-- If `n % 4 = 3`, then `χ₄ n = -1`. -/
+lemma χ₄_nat_three_mod_four {n : ℕ} (hn : n % 4 = 3) : χ₄ n = -1 :=
+by { rw [χ₄_nat_mod_four, hn], refl }
+
+/-- If `n % 4 = 1`, then `χ₄ n = 1`. -/
+lemma χ₄_int_one_mod_four {n : ℤ} (hn : n % 4 = 1) : χ₄ n = 1 :=
+by { rw [χ₄_int_mod_four, hn], refl }
+
+/-- If `n % 4 = 3`, then `χ₄ n = -1`. -/
+lemma χ₄_int_three_mod_four {n : ℤ} (hn : n % 4 = 3) : χ₄ n = -1 :=
+by { rw [χ₄_int_mod_four, hn], refl }
+
 /-- If `n % 4 = 1`, then `(-1)^(n/2) = 1`. -/
 lemma _root_.neg_one_pow_div_two_of_one_mod_four {n : ℕ} (hn : n % 4 = 1) :
   (-1 : ℤ) ^ (n / 2) = 1 :=
@@ -86,6 +110,14 @@ It corresponds to the extension `ℚ(√2)/ℚ`. -/
 /-- `χ₈` takes values in `{0, 1, -1}` -/
 lemma is_quadratic_χ₈ : χ₈.is_quadratic := by { intro a, dec_trivial!, }
 
+/-- The value of `χ₈ n`, for `n : ℕ`, depends only on `n % 8`. -/
+lemma χ₈_nat_mod_eight (n : ℕ) : χ₈ n = χ₈ (n % 8 : ℕ) :=
+by rw ← zmod.nat_cast_mod n 8
+
+/-- The value of `χ₈ n`, for `n : ℤ`, depends only on `n % 8`. -/
+lemma χ₈_int_mod_eight (n : ℤ) : χ₈ n = χ₈ (n % 8 : ℤ) :=
+by { rw ← zmod.int_cast_mod n 8, norm_cast, }
+
 /-- An explicit description of `χ₈` on integers / naturals -/
 lemma χ₈_int_eq_if_mod_eight (n : ℤ) :
   χ₈ n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1 :=

src/ring_theory/int/basic.lean

@@ -176,6 +176,21 @@ end
 lemma coprime_iff_nat_coprime {a b : ℤ} : is_coprime a b ↔ nat.coprime a.nat_abs b.nat_abs :=
 by rw [←gcd_eq_one_iff_coprime, nat.coprime_iff_gcd_eq_one, gcd_eq_nat_abs]
 
+/-- If `gcd a (m * n) ≠ 1`, then `gcd a m ≠ 1` or `gcd a n ≠ 1`. -/
+lemma gcd_ne_one_iff_gcd_mul_right_ne_one {a : ℤ} {m n : ℕ} :
+  a.gcd (m * n) ≠ 1 ↔ a.gcd m ≠ 1 ∨ a.gcd n ≠ 1 :=
+by simp only [gcd_eq_one_iff_coprime, ← not_and_distrib, not_iff_not, is_coprime.mul_right_iff]
+
+/-- If `gcd a (m * n) = 1`, then `gcd a m = 1`. -/
+lemma gcd_eq_one_of_gcd_mul_right_eq_one_left {a : ℤ} {m n : ℕ} (h : a.gcd (m * n) = 1) :
+  a.gcd m = 1 :=
+nat.dvd_one.mp $ trans_rel_left _ (gcd_dvd_gcd_mul_right_right a m n) h
+
+/-- If `gcd a (m * n) = 1`, then `gcd a n = 1`. -/
+lemma gcd_eq_one_of_gcd_mul_right_eq_one_right {a : ℤ} {m n : ℕ} (h : a.gcd (m * n) = 1) :
+  a.gcd n = 1 :=
+nat.dvd_one.mp $ trans_rel_left _ (gcd_dvd_gcd_mul_left_right a n m) h
+
 lemma sq_of_gcd_eq_one {a b c : ℤ} (h : int.gcd a b = 1) (heq : a * b = c ^ 2) :
   ∃ (a0 : ℤ), a = a0 ^ 2 ∨ a = - (a0 ^ 2) :=
 begin