feat(algebra/module/basic): smul_add_hom_one (#7461)

leanprover-community · May 7, 2021 · 190d4e2 · 190d4e2
1 parent 91d5aa6
commit 190d4e2
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git 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
@@ -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