Commit 2021-09-02 12:25 baefdf34

fix(group_theory/group_action/defs): deduplicate const_smul_hom and distrib_mul_action.to_add_monoid_hom (#8953) This removes const_smul_hom as distrib_mul_action.to_add_monoid_hom fits a larger family of similarly-named definitions. This also renames distrib_mul_action.hom_add_monoid_hom to distrib_mul_action.to_add_monoid_End to better match its statement. Zulip thread