Commit 2021-09-08 12:15 a8c5c5a5

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.