mathlib

de37a6aa - chore(field_theory/fixed): reuse existing `mul_semiring_action.to_alg_hom` by providing `smul_comm_class` (#8965)

chore(field_theory/fixed): reuse existing `mul_semiring_action.to_alg_hom` by providing `smul_comm_class` (#8965) This removes `fixed_points.to_alg_hom` as this is really just a bundled form of `mul_semiring_action.to_alg_hom` + `mul_semiring_action.to_alg_hom_injective`, once we provide the missing `smul_comm_class`.