feat(data/polynomial/eval): map_equiv (#9375)

leanprover-community · Sep 25, 2021 · 42d8243 · 42d8243
1 parent 59b9ebb
commit 42d8243
Showing 1 changed file with 8 additions and 0 deletions.
diff --git 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])