diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean
index e98e90767d19c..7e6241a3fc570 100644
--- a/Mathlib/Algebra/Module/LinearMap.lean
+++ b/Mathlib/Algebra/Module/LinearMap.lean
@@ -269,11 +269,17 @@ protected def Simps.apply {R S : Type _} [Semiring R] [Semiring S] (σ : R →+*
 initialize_simps_projections LinearMap (toAddHom_toFun → apply)
 
 @[simp]
-theorem coe_mk {σ : R →+* S} (f : M →+ M₃) (h) :
+theorem coe_mk {σ : R →+* S} (f : AddHom M M₃) (h) :
     ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : M → M₃) = f :=
   rfl
 #align linear_map.coe_mk LinearMap.coe_mk
 
+-- Porting note: This theorem is new.
+@[simp]
+theorem coe_addHom_mk {σ : R →+* S} (f : AddHom M M₃) (h) :
+    ((LinearMap.mk f h : M →ₛₗ[σ] M₃) : AddHom M M₃) = f :=
+  rfl
+
 /-- Identity map as a `LinearMap` -/
 def id : M →ₗ[R] M :=
   { DistribMulActionHom.id R with toFun := _root_.id }