feat(field_theory/normal): Define the normal closure (#16144)
feat(field_theory/normal): Define the normal closure (#16144)

This PR adds the definition of the normal closure, and proves that the normal closure is finite-dimensional and normal.





leanprover-community/mathlib,leanprover-community/mathlib