feat(field_theory/normal): normal_of_alg_equiv (#5225)
feat(field_theory/normal): normal_of_alg_equiv (#5225)

Proves that normal is preserved by an alg_equiv





leanprover-community/mathlib,leanprover-community/mathlib