feat(*): assorted prereqs for cyclotomic polynomials (#4887)

This is hopefully my last preparatory PR for cyclotomic polynomials. It was in [4869](#4869) .


Co-authored-by: Johan Commelin <johan@commelin.net>

Author: riccardobrasca

src/data/polynomial/ring_division.lean

@@ -406,12 +406,12 @@ else by rw [← with_bot.coe_le_coe, ← degree_X_pow_sub_C (nat.pos_of_ne_zero
   exact card_roots (X_pow_sub_C_ne_zero (nat.pos_of_ne_zero hn) a)
 
 /-- The multiset `nth_roots ↑n (1 : R)` as a finset. -/
-def nth_roots_finset (n : ℕ+) (R : Type*) [integral_domain R] : finset R :=
+def nth_roots_finset (n : ℕ) (R : Type*) [integral_domain R] : finset R :=
 multiset.to_finset (nth_roots n (1 : R))
 
-@[simp] lemma mem_nth_roots_finset {n : ℕ+} {x : R} :
+@[simp] lemma mem_nth_roots_finset {n : ℕ} (h : 0 < n) {x : R} :
   x ∈ nth_roots_finset n R ↔ x ^ (n : ℕ) = 1 :=
-by rw [nth_roots_finset, mem_to_finset, mem_nth_roots n.pos]
+by rw [nth_roots_finset, mem_to_finset, mem_nth_roots h]
 
 end nth_roots
 

src/number_theory/divisors.lean

@@ -359,14 +359,14 @@ lemma prod_divisors_prime_pow {α : Type*} [comm_monoid α] {k p : ℕ} {f : ℕ
 @sum_divisors_prime_pow (additive α) _ _ _ _ h
 
 @[simp]
-lemma filter_dvd_eq_divisors (n : ℕ+) :
-  finset.filter (λ (x : ℕ), x ∣ ↑n) (finset.range (n : ℕ).succ) = (n : ℕ).divisors :=
+lemma filter_dvd_eq_divisors {n : ℕ} (h : n ≠ 0) :
+  finset.filter (λ (x : ℕ), x ∣ n) (finset.range (n : ℕ).succ) = (n : ℕ).divisors :=
 begin
   apply finset.ext,
-  simp only [mem_divisors, mem_filter, mem_range, and_true,
-    and_iff_right_iff_imp, ne.def, pnat.ne_zero, not_false_iff],
+  simp only [h, mem_filter, and_true, and_iff_right_iff_imp, cast_id, mem_range, ne.def,
+  not_false_iff, mem_divisors],
   intros a ha,
-  exact nat.lt_succ_of_le (nat.divisor_le (nat.mem_divisors.2 (and.intro ha (pnat.ne_zero n))))
+  exact nat.lt_succ_of_le (nat.divisor_le (nat.mem_divisors.2 ⟨ha, h⟩))
 end
 
 end nat

src/ring_theory/roots_of_unity.lean

@@ -373,6 +373,24 @@ section integral_domain
 
 variables {ζ : R}
 
+@[simp] lemma primitive_roots_zero : primitive_roots 0 R = ∅ :=
+begin
+  rw [← finset.val_eq_zero, ← multiset.subset_zero, ← nth_roots_zero (1 : R), primitive_roots],
+    simp only [finset.not_mem_empty, forall_const, forall_prop_of_false, multiset.to_finset_zero,
+    finset.filter_true_of_mem, finset.empty_val, not_false_iff,
+    multiset.zero_subset, nth_roots_zero]
+end
+
+@[simp] lemma primitive_root_one : primitive_roots 1 R = {(1 : R)} :=
+begin
+  apply finset.eq_singleton_iff_unique_mem.2,
+  split,
+  { simp only [is_primitive_root.one_right_iff, mem_primitive_roots zero_lt_one] },
+  { intros x hx,
+    rw [mem_primitive_roots zero_lt_one, is_primitive_root.one_right_iff] at hx,
+    exact hx }
+end
+
 lemma neg_one (p : ℕ) [char_p R p] (hp : p ≠ 2) : is_primitive_root (-1 : R) 2 :=
 mk_of_lt (-1 : R) dec_trivial (by simp only [one_pow, neg_square]) $
 begin
@@ -562,43 +580,50 @@ end
 
 /-- The cardinality of the multiset `nth_roots ↑n (1 : R)` is `n`
 if there is a primitive root of unity in `R`. -/
-lemma card_nth_roots {ζ : R} {n : ℕ+} (h : is_primitive_root ζ n) :
-  (nth_roots ↑n (1 : R)).card = n :=
+lemma card_nth_roots {ζ : R} {n : ℕ} (h : is_primitive_root ζ n) :
+  (nth_roots n (1 : R)).card = n :=
 begin
+  cases nat.eq_zero_or_pos n with hzero hpos,
+  { simp only [hzero, multiset.card_zero, nth_roots_zero] },
   rw eq_iff_le_not_lt,
-  split,
-  { exact card_nth_roots n 1 },
+  use card_nth_roots n 1,
   { rw [not_lt],
     have hcard : fintype.card {x // x ∈ nth_roots n (1 : R)}
       ≤ (nth_roots n (1 : R)).attach.card := multiset.card_le_of_le (multiset.erase_dup_le _),
     rw multiset.card_attach at hcard,
-    rw [← fintype.card_congr (roots_of_unity_equiv_nth_roots R n), card_roots_of_unity h] at hcard,
+    rw ← pnat.to_pnat'_coe hpos at hcard h ⊢,
+    set m := nat.to_pnat' n,
+    rw [← fintype.card_congr (roots_of_unity_equiv_nth_roots R m), card_roots_of_unity h] at hcard,
     exact hcard }
 end
 
 /-- The multiset `nth_roots ↑n (1 : R)` has no repeated elements
 if there is a primitive root of unity in `R`. -/
-lemma nth_roots_nodup {ζ : R} {n : ℕ+} (h : is_primitive_root ζ n) : (nth_roots ↑n (1 : R)).nodup :=
+lemma nth_roots_nodup {ζ : R} {n : ℕ} (h : is_primitive_root ζ n) : (nth_roots n (1 : R)).nodup :=
 begin
+  cases nat.eq_zero_or_pos n with hzero hpos,
+  { simp only [hzero, multiset.nodup_zero, nth_roots_zero] },
   apply (@multiset.erase_dup_eq_self R _ _).1,
   rw eq_iff_le_not_lt,
   split,
-  { exact multiset.erase_dup_le (nth_roots ↑n (1 : R)) },
+  { exact multiset.erase_dup_le (nth_roots n (1 : R)) },
   { by_contra ha,
     replace ha := multiset.card_lt_of_lt ha,
     rw card_nth_roots h at ha,
-    have hrw : (nth_roots ↑n (1 : R)).erase_dup.card =
-      fintype.card {x // x ∈ (nth_roots ↑n (1 : R))},
-    { set fs := (⟨(nth_roots ↑n (1 : R)).erase_dup, multiset.nodup_erase_dup _⟩ : finset R),
+    have hrw : (nth_roots n (1 : R)).erase_dup.card =
+      fintype.card {x // x ∈ (nth_roots n (1 : R))},
+    { set fs := (⟨(nth_roots n (1 : R)).erase_dup, multiset.nodup_erase_dup _⟩ : finset R),
       rw [← finset.card_mk, ← fintype.card_of_subtype fs _],
       intro x,
       simp only [multiset.mem_erase_dup, finset.mem_mk] },
-    rw [hrw, ← fintype.card_congr (roots_of_unity_equiv_nth_roots R n),
+    rw ← pnat.to_pnat'_coe hpos at h hrw ha,
+    set m := nat.to_pnat' n,
+    rw [hrw, ← fintype.card_congr (roots_of_unity_equiv_nth_roots R m),
         card_roots_of_unity h] at ha,
     exact nat.lt_asymm ha ha }
 end
 
-@[simp] lemma card_nth_roots_finset {ζ : R} {n : ℕ+} (h : is_primitive_root ζ n) :
+@[simp] lemma card_nth_roots_finset {ζ : R} {n : ℕ} (h : is_primitive_root ζ n) :
   (nth_roots_finset n R).card = n :=
 by rw [nth_roots_finset, ← multiset.to_finset_eq (nth_roots_nodup h), card_mk, h.card_nth_roots]
 
@@ -650,7 +675,7 @@ end
 
 /-- `nth_roots n` as a `finset` is equal to the union of `primitive_roots i R` for `i ∣ n`
 if there is a primitive root of unity in `R`. -/
-lemma nth_roots_one_eq_bind_primitive_roots {ζ : R} {n : ℕ+} (h : is_primitive_root ζ n) :
+lemma nth_roots_one_eq_bind_primitive_roots' {ζ : R} {n : ℕ+} (h : is_primitive_root ζ n) :
   nth_roots_finset n R = (nat.divisors ↑n).bind (λ i, (primitive_roots i R)) :=
 begin
   symmetry,
@@ -668,7 +693,7 @@ begin
     rw [hd, pow_mul, ha.pow_eq_one, one_pow] },
   { apply le_of_eq,
     rw [h.card_nth_roots_finset, finset.card_bind],
-    { rw [← nat.sum_totient n, nat.filter_dvd_eq_divisors n, sum_congr rfl]
+    { rw [← nat.sum_totient n, nat.filter_dvd_eq_divisors (pnat.ne_zero n), sum_congr rfl]
         { occs := occurrences.pos [1] },
       simp only [finset.mem_filter, finset.mem_range, nat.mem_divisors],
       rintro k ⟨H, hk⟩,
@@ -681,6 +706,13 @@ begin
       exact disjoint (pnat.pos_of_div_pos hi) (pnat.pos_of_div_pos hj) hdiff } }
 end
 
+/-- `nth_roots n` as a `finset` is equal to the union of `primitive_roots i R` for `i ∣ n`
+if there is a primitive root of unity in `R`. -/
+lemma nth_roots_one_eq_bind_primitive_roots {ζ : R} {n : ℕ} (hpos : 0 < n)
+  (h : is_primitive_root ζ n) :
+  nth_roots_finset n R = (nat.divisors n).bind (λ i, (primitive_roots i R)) :=
+@nth_roots_one_eq_bind_primitive_roots' _ _ _ ⟨n, hpos⟩ h
+
 end integral_domain
 
 end is_primitive_root