feat(algebra/module): linear_map.coe_mk (#1290)

src/algebra/module.lean

@@ -135,6 +135,9 @@ include α
 
 instance : has_coe_to_fun (β →ₗ[α] γ) := ⟨_, to_fun⟩
 
+@[simp] lemma coe_mk (f : β → γ) (h₁ h₂) :
+  ((linear_map.mk f h₁ h₂ : β →ₗ[α] γ) : β → γ) = f := rfl
+
 theorem is_linear : is_linear_map α f := {..f}
 
 @[extensionality] theorem ext {f g : β →ₗ[α] γ} (H : ∀ x, f x = g x) : f = g :=