feat(Polynomial/Roots): add a theorem for computing roots (#32357)

The theorem `roots_eq_of_degree` shows that S is the set of roots of a degree d polynomial P if #S = d and P(x) = 0 for every x in S.

Author: YuvalFilmus

Mathlib/Algebra/Polynomial/Roots.lean

@@ -286,6 +286,20 @@ theorem card_roots_X_pow_sub_C {n : ℕ} (hn : 0 < n) (a : R) :
         card_roots (X_pow_sub_C_ne_zero hn a)
       _ = n := degree_X_pow_sub_C hn a
 
+theorem roots_eq_of_degree_le_card_of_ne_zero {S : Finset R}
+    (hS : ∀ x ∈ S, p.eval x = 0) (hcard : p.degree ≤ S.card) (hp : p ≠ 0) : p.roots = S.val := by
+  refine (Multiset.eq_of_le_of_card_le ?_ ?_).symm
+  · exact (Finset.val_le_iff_val_subset.mpr (fun x hx ↦ (p.mem_roots hp).mpr (hS x hx)))
+  · simpa using (p.card_roots hp).trans hcard
+
+theorem roots_eq_of_degree_le_card {S : Finset R}
+    (hS : ∀ x ∈ S, p.eval x = 0) (hcard : S.card = p.degree) : p.roots = S.val :=
+  roots_eq_of_degree_le_card_of_ne_zero hS (by lia) (by contrapose! hcard; simp [hcard])
+
+theorem roots_eq_of_natDegree_le_card_of_ne_zero {S : Finset R}
+    (hS : ∀ x ∈ S, p.eval x = 0) (hcard : p.natDegree ≤ S.card) (hp : p ≠ 0) : p.roots = S.val :=
+  roots_eq_of_degree_le_card_of_ne_zero hS (degree_le_of_natDegree_le hcard) hp
+
 section NthRoots
 
 /-- `nthRoots n a` noncomputably returns the solutions to `x ^ n = a`. -/