diff --git a/src/algebra/module/basic.lean b/src/algebra/module/basic.lean
index 4a6b21c9c1e20..13d72219b2cac 100644
--- a/src/algebra/module/basic.lean
+++ b/src/algebra/module/basic.lean
@@ -119,6 +119,10 @@ 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 _ :=
+const_smul_hom_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]
 
diff --git a/src/group_theory/group_action/defs.lean b/src/group_theory/group_action/defs.lean
index d9ed1a482ea43..5ee201115a1ad 100644
--- a/src/group_theory/group_action/defs.lean
+++ b/src/group_theory/group_action/defs.lean
@@ -308,6 +308,10 @@ variable {A}
 @[simp] lemma const_smul_hom_apply (r : M) (x : A) :
   const_smul_hom A r x = r • x := rfl
 
+@[simp] lemma const_smul_hom_one :
+  const_smul_hom A (1:M) = add_monoid_hom.id _ :=
+by { ext, rw [const_smul_hom_apply, one_smul, add_monoid_hom.id_apply] }
+
 end
 
 section