mathlib3

20f68fc8 - feat(field_theory/splitting_field): If an intermediate field contains all of the roots, then the polynomial splits (#15658)

feat(field_theory/splitting_field): If an intermediate field contains all of the roots, then the polynomial splits (#15658) This lemma came up when proving that if `p` splits in `L/K`, then `p.is_splitting_field K (adjoin K (p.root_set L))` Co-authored-by: tb65536 <tb65536@users.noreply.github.com>