mathlib

a8c5c5a5 - feat(algebra/module/basic): add `module.to_add_monoid_End` (#8968)

feat(algebra/module/basic): add `module.to_add_monoid_End` (#8968) I also removed `smul_add_hom_one` since it's a special case of the ring_hom. I figured I'd replace a `simp` with a `rw` when fixing `finsupp.to_free_abelian_group_comp_to_finsupp` for this removal.