mathlib3

d5d2c4f6 - feat(field_theory/splitting_field): add a more general algebra instance as a def (#10220)

feat(field_theory/splitting_field): add a more general algebra instance as a def (#10220) Unfortunately this def results in the following non-defeq diamonds in `splitting_field_aux.algebra` and `splitting_field.algebra`: ```lean example (n : ℕ) {K : Type u} [field K] {f : polynomial K} (hfn : f.nat_degree = n) : (add_comm_monoid.nat_module : module ℕ (splitting_field_aux n f hfn)) = @algebra.to_module _ _ _ _ (splitting_field_aux.algebra n _ hfn) := rfl --fail example : (add_comm_group.int_module _ : module ℤ (splitting_field_aux n f hfn)) = @algebra.to_module _ _ _ _ (splitting_field_aux.algebra f) := rfl --fail ``` For this reason, we do not make `splitting_field.algebra` an instance by default. The `splitting_field_aux.algebra` instance is less harmful as it is an implementation detail. However, the new def is still perfectly good for recovering the old less-general instance, and avoids the need for `restrict_scalars.algebra`.