mathlib

fae3ce12 - feat(field_theory/splitting_field): Adjoining all of the roots of a polynomial gives a splitting field (#15795)

feat(field_theory/splitting_field): Adjoining all of the roots of a polynomial gives a splitting field (#15795) This PR proves that if `p` splits in a field extensions, then adjoining all of the roots of `p` gives a splitting field of `p`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>