Commit 2022-07-28 04:54 123f4542

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.