mathlib

17ab30b2 - 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.