A polynomial that attains its degree in distinct roots is separable

A polynomial has at most natDegree p roots counted with multiplicity, and at most that many distinct ones. If it has at least that many distinct roots then both bounds are equalities: it splits, and none of its roots repeats — which is separability.

No closure assumption is needed. The root count already forces p to split, by Polynomial.roots_eq_of_natDegree_le_card_of_ne_zero and Polynomial.splits_iff_card_roots; assuming an algebraically closed field would only be a way of guaranteeing the hypothesis, not of using it.

Mathlib has the corresponding equivalence as Polynomial.card_rootSet_eq_natDegree_iff_of_splits, phrased with rootSet over an extension and with splitting and equality as hypotheses. A counting argument supplies none of those: it supplies a lower bound on the number of roots in the field itself. This is that form, and it is the shape every root-counting proof of separability ends in.

Main results

• Polynomial.separable_of_natDegree_le_card_roots

theorem Polynomial.separable_of_natDegree_le_card_roots {F : Type u_1} [Field F] [DecidableEq F] {p : Polynomial F} (hp : p ≠ 0) (h : p.natDegree ≤ p.roots.toFinset.card) : p.Separable

A polynomial with at least as many distinct roots as its degree is separable. The hypothesis is a lower bound because that is what a counting argument gives; the reverse inequality always holds, and the two together force p to split with distinct roots.