From fc87598514c3ebcbc83118dfcdb436a92099daa7 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 3 Apr 2021 14:32:04 +0000 Subject: [PATCH] chore(data/polynomial/eval): add `map_ring_hom_{id,comp}` lemmas (#7019) --- src/data/polynomial/eval.lean | 7 +++++++ 1 file changed, 7 insertions(+) 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))