feat(Polynomial/Splits): dvd_iff_roots_le_roots (#18800)

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>

Author: ChrisHughes24

Mathlib/Algebra/Polynomial/Splits.lean

@@ -322,6 +322,18 @@ theorem eq_prod_roots_of_splits_id {p : K[X]} (hsplit : Splits (RingHom.id K) p)
     p = C p.leadingCoeff * (p.roots.map fun a => X - C a).prod := by
   simpa using eq_prod_roots_of_splits hsplit
 
+theorem Splits.dvd_of_roots_le_roots {p q : K[X]} (hp : p.Splits (RingHom.id _)) (hp0 : p ≠ 0)
+    (hq : p.roots ≤ q.roots) : p ∣ q := by
+  rw [eq_prod_roots_of_splits_id hp, C_mul_dvd (leadingCoeff_ne_zero.2 hp0)]
+  exact dvd_trans
+    (Multiset.prod_dvd_prod_of_le (Multiset.map_le_map hq))
+    (prod_multiset_X_sub_C_dvd _)
+
+theorem Splits.dvd_iff_roots_le_roots {p q : K[X]}
+    (hp : p.Splits (RingHom.id _)) (hp0 : p ≠ 0) (hq0 : q ≠ 0) :
+    p ∣ q ↔ p.roots ≤ q.roots :=
+  ⟨Polynomial.roots.le_of_dvd hq0, hp.dvd_of_roots_le_roots hp0⟩
+
 theorem aeval_eq_prod_aroots_sub_of_splits [Algebra K L] {p : K[X]}
     (hsplit : Splits (algebraMap K L) p) (v : L) :
     aeval v p = algebraMap K L p.leadingCoeff * ((p.aroots L).map fun a ↦ v - a).prod := by