mathlib3

62b5bb74 - refactor(field_theory/*): Refactor `normal` to use `is_algebraic` (#15421)

refactor(field_theory/*): Refactor `normal` to use `is_algebraic` (#15421) This PR refactors `normal` to use `is_algebraic` rather than `is_integral`, as suggested by a TODO comment. I think the motivation is that `is_algebraic` is the preferred language when discussing fields.