mathlib

551079b0 - feat(field_theory/normal): A compositum of normal extensions is normal (#16076)

feat(field_theory/normal): A compositum of normal extensions is normal (#16076) This PR proves that a compositum of normal extensions is normal. The proof uses a technical lemma `exists_finset_of_mem_supr''` to reduce to the case of a finite compositum of finite normal extensions (i.e., a finite compositum of splitting fields), which is proved in `is_splitting_field_supr`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>