Commit 2022-08-04 15:03 20f68fc8

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))