chore(Algebra/Algebra/Hom): automated extraction from #37745 (#43295)

This PR was automatically created from PR #37745 by @AntoineChambert-Loir via a [review comment](#37745 (comment)) by @jcommelin.

Co-authored-by: AntoineChambert-Loir <4817348+AntoineChambert-Loir@users.noreply.github.com>

Author: mathlib-splicebot[bot]

Mathlib/Algebra/Algebra/Hom.lean

@@ -277,6 +277,9 @@ def toLinearMap : A →ₗ[R] B where
   map_add' := map_add _
   map_smul' := map_smul _
 
+theorem toLinearMap_eq_coe (f : A →ₐ[R] B) : f.toLinearMap = f :=
+  rfl
+
 @[simp]
 theorem toLinearMap_apply (p : A) : φ.toLinearMap p = φ p :=
   rfl