feat(data/polynomial/ring_division): add `polynomial.card_le_degree_o…

…f_subset_roots` (#10824)





Co-authored-by: Iván Sadofschi Costa <isadofschi@users.noreply.github.com>

src/data/polynomial/ring_division.lean

@@ -344,6 +344,10 @@ end
 @[simp] lemma mem_roots (hp : p ≠ 0) : a ∈ p.roots ↔ is_root p a :=
 by rw [← count_pos, count_roots p, root_multiplicity_pos hp]
 
+theorem card_le_degree_of_subset_roots {p : polynomial R} {Z : finset R} (h : Z.val ⊆ p.roots) :
+  Z.card ≤ p.nat_degree :=
+(multiset.card_le_of_le (finset.val_le_iff_val_subset.2 h)).trans (polynomial.card_roots' p)
+
 lemma eq_zero_of_infinite_is_root
   (p : polynomial R) (h : set.infinite {x | is_root p x}) : p = 0 :=
 begin