diff --git a/src/data/polynomial/eval.lean b/src/data/polynomial/eval.lean
index fe928aa92add7..370de5627d45b 100644
--- a/src/data/polynomial/eval.lean
+++ b/src/data/polynomial/eval.lean
@@ -560,6 +560,13 @@ def map_ring_hom (f : R →+* S) : polynomial R →+* polynomial S :=
 
 @[simp] lemma coe_map_ring_hom (f : R →+* S) : ⇑(map_ring_hom f) = map f := rfl
 
+@[simp] lemma map_ring_hom_id : map_ring_hom (ring_hom.id R) = ring_hom.id (polynomial R) :=
+ring_hom.ext $ λ x, map_id
+
+@[simp] lemma map_ring_hom_comp [semiring T] (f : S →+* T) (g : R →+* S) :
+  (map_ring_hom f).comp (map_ring_hom g) = map_ring_hom (f.comp g) :=
+ring_hom.ext $ map_map g f
+
 lemma map_list_prod (L : list (polynomial R)) : L.prod.map f = (L.map $ map f).prod :=
 eq.symm $ list.prod_hom _ (monoid_hom.of (map f))