feat(polynomial/cyclotomic): some divisibility results (#12426)

Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

src/data/finset/basic.lean

@@ -1112,6 +1112,8 @@ instance : generalized_boolean_algebra (finset α) :=
 lemma not_mem_sdiff_of_mem_right (h : a ∈ t) : a ∉ s \ t :=
 by simp only [mem_sdiff, h, not_true, not_false_iff, and_false]
 
+lemma not_mem_sdiff_of_not_mem_left (h : a ∉ s) : a ∉ s \ t := by simpa
+
 lemma union_sdiff_of_subset (h : s ⊆ t) : s ∪ (t \ s) = t := sup_sdiff_cancel_right h
 
 theorem sdiff_union_of_subset {s₁ s₂ : finset α} (h : s₁ ⊆ s₂) : (s₂ \ s₁) ∪ s₁ = s₂ :=

src/data/polynomial/eval.lean

@@ -792,6 +792,10 @@ end eval
 
 section map
 
+--TODO rename to `map_dvd_map`
+lemma map_dvd {R S} [semiring R] [comm_semiring S] (f : R →+* S) {x y : R[X]} :
+  x ∣ y → x.map f ∣ y.map f := eval₂_dvd _ _
+
 variables [comm_semiring R] [comm_semiring S] (f : R →+* S)
 
 protected lemma map_multiset_prod (m : multiset R[X]) : m.prod.map f = (m.map $ map f).prod :=

src/ring_theory/polynomial/cyclotomic/basic.lean

@@ -423,6 +423,48 @@ begin
            geom_sum_mul, prod_cyclotomic_eq_X_pow_sub_one h]
 end
 
+lemma cyclotomic_dvd_geom_sum_of_dvd (R) [comm_ring R] {d n : ℕ} (hdn : d ∣ n)
+  (hd : d ≠ 1) : cyclotomic d R ∣ geom_sum X n :=
+begin
+  suffices : (cyclotomic d ℤ).map (int.cast_ring_hom R) ∣ (geom_sum X n).map (int.cast_ring_hom R),
+  { have key := (map_ring_hom (int.cast_ring_hom R)).map_geom_sum X n,
+    simp only [coe_map_ring_hom, map_X] at key,
+    rwa [map_cyclotomic, key] at this },
+  apply map_dvd,
+  rcases n.eq_zero_or_pos with rfl | hn,
+  { simp },
+  rw ←prod_cyclotomic_eq_geom_sum hn,
+  apply finset.dvd_prod_of_mem,
+  simp [hd, hdn, hn.ne']
+end
+
+lemma X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd (R) [comm_ring R] {d n : ℕ}
+  (h : d ∈ n.proper_divisors) :
+  (X ^ d - 1) * ∏ x in n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1 :=
+begin
+  obtain ⟨hd, hdn⟩ := nat.mem_proper_divisors.mp h,
+  have h0n := pos_of_gt hdn,
+  rcases d.eq_zero_or_pos with rfl | h0d,
+  { exfalso, linarith [eq_zero_of_zero_dvd hd] },
+  rw [←prod_cyclotomic_eq_X_pow_sub_one h0d, ←prod_cyclotomic_eq_X_pow_sub_one h0n,
+      mul_comm, finset.prod_sdiff (nat.divisors_subset_of_dvd h0n.ne' hd)]
+end
+
+lemma X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd (R) [comm_ring R] {d n : ℕ}
+  (h : d ∈ n.proper_divisors) : (X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1 :=
+begin
+  have hdn := (nat.mem_proper_divisors.mp h).2,
+  use ∏ x in n.proper_divisors \ d.divisors, cyclotomic x R,
+  symmetry,
+  convert X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd R h using 1,
+  rw mul_assoc,
+  congr' 1,
+  rw [nat.divisors_eq_proper_divisors_insert_self_of_pos $ pos_of_gt hdn,
+      finset.insert_sdiff_of_not_mem, finset.prod_insert],
+  { exact finset.not_mem_sdiff_of_not_mem_left nat.proper_divisors.not_self_mem },
+  { exact λ hk, hdn.not_le $ nat.divisor_le hk }
+end
+
 lemma _root_.is_root_of_unity_iff {n : ℕ} (h : 0 < n) (R : Type*) [comm_ring R] [is_domain R]
   {ζ : R} : ζ ^ n = 1 ↔ ∃ i ∈ n.divisors, (cyclotomic i R).is_root ζ :=
 by rw [←mem_nth_roots h, nth_roots, mem_roots $ X_pow_sub_C_ne_zero h _,