[Merged by Bors] - refactor(polynomial/*): make polynomials irreducible

src/data/mv_polynomial/basic.lean

@@ -203,7 +203,7 @@ by rw [X_pow_eq_single, monomial, monomial, monomial, single_mul_single]; simp
 lemma monomial_single_add : monomial (single n e + s) a = (X n ^ e * monomial s a) :=
 by rw [X_pow_eq_single, monomial, monomial, monomial, single_mul_single]; simp
 
-lemma single_eq_C_mul_X {s : σ} {a : R} {n : ℕ} :
+lemma monomial_eq_C_mul_X {s : σ} {a : R} {n : ℕ} :
   monomial (single s n) a = C a * (X s)^n :=
 by rw [← zero_add (single s n), monomial_add_single, C_apply]
 
@@ -218,7 +218,7 @@ add_monoid_algebra.single_mul_single
 @[simp] lemma monomial_zero {s : σ →₀ ℕ}: monomial s (0 : R) = 0 :=
 single_zero
 
-@[simp] lemma sum_monomial  {A : Type*} [add_comm_monoid A]
+@[simp] lemma sum_monomial_eq  {A : Type*} [add_comm_monoid A]
   {u : σ →₀ ℕ} {r : R} {b : (σ →₀ ℕ) → R → A} (w : b u 0 = 0) :
   sum (monomial u r) b = b u r :=
 sum_single_index w

src/data/mv_polynomial/pderiv.lean

@@ -72,7 +72,7 @@ def pderiv (i : σ) : mv_polynomial σ R →ₗ[R] mv_polynomial σ R :=
 @[simp]
 lemma pderiv_monomial {i : σ} :
   pderiv i (monomial s a) = monomial (s - single i 1) (a * (s i)) :=
-by simp only [pderiv, monomial_zero, sum_monomial, zero_mul, linear_map.coe_mk]
+by simp only [pderiv, monomial_zero, sum_monomial_eq, zero_mul, linear_map.coe_mk]
 
 
 @[simp]

src/data/polynomial/algebra_map.lean

@@ -28,7 +28,20 @@ variables [comm_semiring R] {p q r : polynomial R}
 variables [semiring A] [algebra R A]
 
 /-- Note that this instance also provides `algebra R (polynomial R)`. -/
-instance algebra_of_algebra : algebra R (polynomial A) := add_monoid_algebra.algebra
+instance algebra_of_algebra : algebra R (polynomial A) :=
+{ smul_def' := λ r p, begin
+    rcases p,
+    simp only [C, monomial, monomial_fun, ring_hom.coe_mk, ring_hom.to_fun_eq_coe,
+      function.comp_app, ring_hom.coe_comp, smul_to_finsupp, mul_to_finsupp],
+    exact algebra.smul_def' _ _,
+  end,
+  commutes' := λ r p, begin
+    rcases p,
+    simp only [C, monomial, monomial_fun, ring_hom.coe_mk, ring_hom.to_fun_eq_coe,
+      function.comp_app, ring_hom.coe_comp, mul_to_finsupp],
+    convert algebra.commutes' r p,
+  end,
+  .. C.comp (algebra_map R A) }
 
 lemma algebra_map_apply (r : R) :
   algebra_map R (polynomial A) r = C (algebra_map R A r) :=
@@ -62,7 +75,7 @@ lemma alg_hom_eval₂_algebra_map
   (p : polynomial R) (f : A →ₐ[R] B) (a : A) :
   f (eval₂ (algebra_map R A) a p) = eval₂ (algebra_map R B) (f a) p :=
 begin
-  dsimp [eval₂, finsupp.sum],
+  dsimp [eval₂, sum],
   simp only [f.map_sum, f.map_mul, f.map_pow, ring_hom.eq_int_cast, ring_hom.map_int_cast,
     alg_hom.commutes],
 end
@@ -73,7 +86,7 @@ lemma eval₂_algebra_map_X {R A : Type*} [comm_ring R] [ring A] [algebra R A]
   eval₂ (algebra_map R A) (f X) p = f p :=
 begin
   conv_rhs { rw [←polynomial.sum_C_mul_X_eq p], },
-  dsimp [eval₂, finsupp.sum],
+  dsimp [eval₂, sum],
   simp only [f.map_sum, f.map_mul, f.map_pow, ring_hom.eq_int_cast, ring_hom.map_int_cast],
   simp [polynomial.C_eq_algebra_map],
 end
@@ -108,7 +121,11 @@ def aeval : polynomial R →ₐ[R] A :=
 variables {R A}
 
 @[ext] lemma alg_hom_ext {f g : polynomial R →ₐ[R] A} (h : f X = g X) : f = g :=
-by { ext, exact h }
+begin
+  ext p,
+  rw [← sum_monomial_eq p],
+  simp [sum, f.map_sum, g.map_sum, monomial_eq_smul_X, h],
+end
 
 theorem aeval_def (p : polynomial R) : aeval x p = eval₂ (algebra_map R A) x p := rfl
 
@@ -212,15 +229,15 @@ begin
   by_cases hf : f = 0,
   { simp [hf] },
   by_cases hi : i ∈ f.support,
-  { rw [eval, eval₂, sum_def] at dvd_eval,
+  { rw [eval, eval₂, sum] at dvd_eval,
     rw [←finset.insert_erase hi, finset.sum_insert (finset.not_mem_erase _ _)] at dvd_eval,
     refine (dvd_add_left _).mp dvd_eval,
     apply finset.dvd_sum,
     intros j hj,
     exact dvd_terms j (finset.ne_of_mem_erase hj) },
   { convert dvd_zero p,
-    convert _root_.zero_mul _,
-    exact finsupp.not_mem_support_iff.mp hi }
+    rw not_mem_support_iff at hi,
+    simp [hi] }
 end
 
 lemma dvd_term_of_is_root_of_dvd_terms {r p : S} {f : polynomial S} (i : ℕ)