mathlib3
df76f433 - chore(field_theory/splitting_field): split file (#19154)

Commit
2 years ago
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.
Parents
Loading