diff --git a/src/data/polynomial/eval.lean b/src/data/polynomial/eval.lean
index 2ea732a6c597c..de3d21442d627 100644
--- a/src/data/polynomial/eval.lean
+++ b/src/data/polynomial/eval.lean
@@ -507,6 +507,14 @@ begin
   split_ifs; simp [f.map_zero],
 end
 
+/-- If `R` and `S` are isomorphic, then so are their polynomial rings. -/
+@[simps] def map_equiv (e : R ≃+* S) : polynomial R ≃+* polynomial S :=
+ring_equiv.of_hom_inv
+  (map_ring_hom e)
+  (map_ring_hom e.symm)
+  (by ext; simp)
+  (by ext; simp)
+
 lemma map_map [semiring T] (g : S →+* T)
   (p : polynomial R) : (p.map f).map g = p.map (g.comp f) :=
 ext (by simp [coeff_map])