From 5000fb0242909099b984e11951d93ca555a18687 Mon Sep 17 00:00:00 2001
From: Eric <ericrboidi@gmail.com>
Date: Fri, 19 Nov 2021 08:56:27 +0000
Subject: [PATCH] feat(data/polynomial/eval): is_root_(prod/map) (#10360)

Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>
---
 src/data/polynomial/eval.lean | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/src/data/polynomial/eval.lean b/src/data/polynomial/eval.lean
index dcb9f584e5445..33a05ca1606ef 100644
--- a/src/data/polynomial/eval.lean
+++ b/src/data/polynomial/eval.lean
@@ -345,6 +345,8 @@ instance [decidable_eq R] : decidable (is_root p a) := by unfold is_root; apply_
 
 @[simp] lemma is_root.def : is_root p a ↔ p.eval a = 0 := iff.rfl
 
+lemma is_root.eq_zero (h : is_root p x) : eval x p = 0 := h
+
 lemma coeff_zero_eq_eval_zero (p : polynomial R) :
   coeff p 0 = p.eval 0 :=
 calc coeff p 0 = coeff p 0 * 0 ^ 0 : by simp
@@ -755,6 +757,11 @@ begin
     rw [h0, ← hpj, finset.prod_insert hj, eval_mul] },
 end
 
+lemma is_root_prod {R} [comm_ring R] [is_domain R] {ι : Type*}
+  (s : finset ι) (p : ι → polynomial R) (x : R) :
+  is_root (∏ j in s, p j) x ↔ ∃ i ∈ s, is_root (p i) x :=
+by simp only [is_root, eval_prod, finset.prod_eq_zero_iff]
+
 end eval
 
 section map
@@ -779,6 +786,18 @@ begin
   exact ring_hom.map_zero f,
 end
 
+lemma is_root.map {f : R →+* S} {x : R} {p : polynomial R} (h : is_root p x) :
+  is_root (p.map f) (f x) :=
+by rw [is_root, eval_map, eval₂_hom, h.eq_zero, f.map_zero]
+
+lemma is_root.of_map {R} [comm_ring R] {f : R →+* S} {x : R} {p : polynomial R}
+  (h : is_root (p.map f) (f x)) (hf : function.injective f) : is_root p x :=
+by rwa [is_root, ←f.injective_iff'.mp hf, ←eval₂_hom, ←eval_map]
+
+lemma is_root_map_iff {R : Type*} [comm_ring R] {f : R →+* S} {x : R} {p : polynomial R}
+  (hf : function.injective f) : is_root (p.map f) (f x) ↔ is_root p x :=
+⟨λ h, h.of_map hf, λ h, h.map⟩
+
 end map
 
 end comm_semiring