Commit 2023-06-05 05:15 df76f433

chore(field_theory/splitting_field): split file (#19154) We split field_theory.splitting_field into field_theory.splitting_field.is_splitting_field and field_theory.splitting_field.construction. This is useful for the port, but also quite a lot of Galois theory should not depend on the existence of splitting fields.