mathlib

901c5bca - feat(ring_theory/separable): a separable polynomial splits into a product of unique `X - C a` (#3877)

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. Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>