Commit 2020-08-20 21:33 901c5bca
View on Github →feat(ring_theory/separable): a separable polynomial splits into a product of unique X - C a (#3877)
Bonus result: the degree of a separable polynomial is the number of roots
in the field where it splits.