mathlib3

123f4542 - chore(field_theory/splitting_field): remove unneeded parameter (#15716)

chore(field_theory/splitting_field): remove unneeded parameter (#15716) The definition of `splitting_field_aux` relied on a parameter `hfn : n = f.nat_degree` that was never actually used in the construction or its instances, only in the `splits` theorem. So we might as well delete it. This PR prepares for a redefinition of all instances on `splitting_field_aux` to fix instance diamonds, see the `splitting_field-diamond` branch for progress. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>