mathlib3

8b6f541e - feat(field_theory/normal): Splitting field is normal (#5768)

feat(field_theory/normal): Splitting field is normal (#5768) Proves that splitting fields are normal. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>