mathlib3

e95928c0 - feat(field_theory/normal): Restrict to normal subfield (#5845)

feat(field_theory/normal): Restrict to normal subfield (#5845) Now that we know that splitting fields are normal, it makes sense to move the results of #5562 to `normal.lean`.