mathlib3

e3f4be1f - chore(field_theory/splitting_field): refactor `splitting_field` (#19178)

chore(field_theory/splitting_field): refactor `splitting_field` (#19178) We refactor the definition of `splitting_field`. The main motivation is to backport [!4#4891](https://github.com/leanprover-community/mathlib4/pull/4891) since the is seems very problematic to port the current design. Zulip discussion relevant to this PR: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234891.20.20FieldTheory.2ESplittingField