feat(algebra/ring/basic): coercions of ring_hom.id (#8439)

Two basic lemmas about the identity map as a ring hom, split off from #3292 at @eric-wieser's suggestion.

Author: alexjbest

src/algebra/ring/basic.lean

@@ -462,6 +462,8 @@ include rα
 instance : inhabited (α →+* α) := ⟨id α⟩
 
 @[simp] lemma id_apply (x : α) : ring_hom.id α x = x := rfl
+@[simp] lemma coe_add_monoid_hom_id : (id α : α →+ α) = add_monoid_hom.id α := rfl
+@[simp] lemma coe_monoid_hom_id : (id α : α →* α) = monoid_hom.id α := rfl
 
 variable {rγ : non_assoc_semiring γ}
 include rβ rγ