feat(data/polynomial): adds map_comp (#3736)

Adds lemma saying that the map of the composition of two polynomials is the composition of the maps, as mentioned [here](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Polynomial.20composition.20and.20map.20commute).

Co-authored-by: Thomas Browning tb65536@uw.edu

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Author: pglutz

src/algebra/big_operators/basic.lean

@@ -549,6 +549,14 @@ begin
   exact ⟨x, (mem_filter.1 hx).1, (mem_filter.1 hx).2⟩
 end
 
+@[to_additive]
+lemma prod_subset_one_on_sdiff [decidable_eq α] (h : s₁ ⊆ s₂) (hg : ∀ x ∈ (s₂ \ s₁), g x = 1)
+  (hfg : ∀ x ∈ s₁, f x = g x) : ∏ i in s₁, f i = ∏ i in s₂, g i :=
+begin
+  rw [← prod_sdiff h, prod_eq_one hg, one_mul],
+  exact prod_congr rfl hfg
+end
+
 lemma sum_range_succ {β} [add_comm_monoid β] (f : ℕ → β) (n : ℕ) :
   (∑ x in range (n + 1), f x) = f n + (∑ x in range n, f x) :=
 by rw [range_succ, sum_insert not_mem_range_self]

src/data/polynomial/eval.lean

@@ -447,6 +447,28 @@ lemma map_prod {ι : Type*} (g : ι → polynomial R) (s : finset ι) :
   (∏ i in s, g i).map f = ∏ i in s, (g i).map f :=
 eq.symm $ prod_hom _ _
 
+lemma map_sum {ι : Type*} (g : ι → polynomial R) (s : finset ι) :
+  (∑ i in s, g i).map f = ∑ i in s, (g i).map f :=
+eq.symm $ sum_hom _ _
+
+lemma support_map_subset (p : polynomial R) : (map f p).support ⊆ p.support :=
+begin
+  intros x,
+  simp only [mem_support_iff],
+  contrapose!,
+  change p.coeff x = 0 → (map f p).coeff x = 0,
+  rw coeff_map,
+  intro hx,
+  rw hx,
+  exact ring_hom.map_zero f,
+end
+
+lemma map_comp (p q : polynomial R) : map f (p.comp q) = (map f p).comp (map f q) :=
+polynomial.induction_on p
+  (by simp)
+  (by simp {contextual := tt})
+  (by simp [pow_succ', ← mul_assoc, polynomial.comp] {contextual := tt})
+
 end map
 
 end comm_semiring