Factorwise separability of a polynomial (source code)

= Factorwise separability of a polynomial

A nonzero <polynomial> is factorwise separable if every irreducible factor is a <separable polynomial>. Unlike the convention that all roots must be distinct, this condition allows repeated irreducible factors. Its <splitting field> is a <separable field extension> precisely when the polynomial is factorwise separable: in one direction every root has a separable minimal polynomial; in the other, adjoining finitely many roots with separable minimal polynomials gives a separable extension. Thus the implication from a separable splitting extension to a polynomial with distinct roots needs the extra squarefree hypothesis. The example $(X-1)^2$ already distinguishes the conventions.