theorem card_roots_le_deg {K : Type u_1} [CommRing K] [IsDomain K] (p : Polynomial K) : p.roots.toFinset.card ≤ p.natDegree

A polynomial of degree d over an integral domain has at most d distinct roots.