mathlib

7afd66ab - feat(field_theory/intermediate_field): Produce an intermediate field from a subalgebra satisfying `is_field`. (#15659)

feat(field_theory/intermediate_field): Produce an intermediate field from a subalgebra satisfying `is_field`. (#15659) This construction came up when proving that if `p` splits in `L/K`, then `p.is_splitting_field K (adjoin K (p.root_set L))`.