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.

src/algebra/module/basic.lean

@@ -112,21 +112,25 @@ See note [reducible non-instances]. -/
 
 variables (R) (M)
 
-/-- `(•)` as an `add_monoid_hom`. -/
+/-- `(•)` as an `add_monoid_hom`.
+
+This is a stronger version of `distrib_mul_action.to_add_monoid_End` -/
+@[simps apply_apply]
+def module.to_add_monoid_End : R →+* add_monoid.End M :=
+{ map_zero' := add_monoid_hom.ext $ λ r, by simp,
+  map_add' := λ x y, add_monoid_hom.ext $ λ r, by simp [add_smul],
+  ..distrib_mul_action.to_add_monoid_End R M }
+
+/-- A convenience alias for `module.to_add_monoid_End` as a `monoid_hom`, usually to allow the
+use of `add_monoid_hom.flip`. -/
 def smul_add_hom : R →+ M →+ M :=
-{ to_fun := distrib_mul_action.to_add_monoid_hom M,
-  map_zero' := add_monoid_hom.ext $ λ r, by simp,
-  map_add' := λ x y, add_monoid_hom.ext $ λ r, by simp [add_smul] }
+(module.to_add_monoid_End R M).to_add_monoid_hom
 
 variables {R M}
 
 @[simp] lemma smul_add_hom_apply (r : R) (x : M) :
   smul_add_hom R M r x = r • x := rfl
 
-@[simp] lemma smul_add_hom_one {R M : Type*} [semiring R] [add_comm_monoid M] [module R M] :
-  smul_add_hom R M 1 = add_monoid_hom.id _ :=
-(distrib_mul_action.to_add_monoid_End R M).map_one
-
 lemma module.eq_zero_of_zero_eq_one (zero_eq_one : (0 : R) = 1) : x = 0 :=
 by rw [←one_smul R x, ←zero_eq_one, zero_smul]
 

src/group_theory/free_abelian_group_finsupp.lean

@@ -53,16 +53,16 @@ begin
   rw [add_monoid_hom.comp_assoc, finsupp.to_free_abelian_group_comp_single_add_hom],
   simp only [to_finsupp, add_monoid_hom.coe_comp, finsupp.single_add_hom_apply,
     function.comp_app, one_smul, lift.of, add_monoid_hom.flip_apply,
-    smul_add_hom_one, add_monoid_hom.id_apply],
+    smul_add_hom_apply, add_monoid_hom.id_apply],
 end
 
 @[simp] lemma finsupp.to_free_abelian_group_comp_to_finsupp :
   to_free_abelian_group.comp to_finsupp = add_monoid_hom.id (free_abelian_group X) :=
 begin
   ext,
-  simp only [to_free_abelian_group, to_finsupp, finsupp.lift_add_hom_apply_single,
-    add_monoid_hom.coe_comp, function.comp_app, one_smul, add_monoid_hom.id_apply, lift.of,
-    add_monoid_hom.flip_apply, smul_add_hom_one],
+  rw [to_free_abelian_group, to_finsupp, add_monoid_hom.comp_apply, lift.of,
+    lift_add_hom_apply_single, add_monoid_hom.flip_apply, smul_add_hom_apply, one_smul,
+    add_monoid_hom.id_apply],
 end
 
 @[simp] lemma finsupp.to_free_abelian_group_to_finsupp {X} (x : free_abelian_group X) :