feat(data/polynomial): Add polynomial/eval lemmas (#3876)

Add some lemmas about `polynomial`. In particular, add lemmas about
`eval2` for the case that the ring `S` that we evaluate into is
non-commutative.




Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>

src/data/polynomial/degree/basic.lean

@@ -588,7 +588,6 @@ decidable.by_cases
     by rw [leading_coeff_mul', leading_coeff_X_pow, mul_one];
       rwa [leading_coeff_X_pow, mul_one])
 
-
 lemma nat_degree_mul_le {p q : polynomial R} : nat_degree (p * q) ≤ nat_degree p + nat_degree q :=
 begin
   apply nat_degree_le_of_degree_le,
@@ -766,6 +765,14 @@ begin
       exact mul_ne_zero (mt leading_coeff_eq_zero.1 hp) (mt leading_coeff_eq_zero.1 hq) } }
 end
 
+@[simp] lemma leading_coeff_X_add_C (a b : R) (ha : a ≠ 0):
+  leading_coeff (C a * X + C b) = a :=
+begin
+  rw [add_comm, leading_coeff_add_of_degree_lt],
+  { simp },
+  { simpa [degree_C ha] using lt_of_le_of_lt degree_C_le (with_bot.coe_lt_coe.2 zero_lt_one)}
+end
+
 /-- `polynomial.leading_coeff` bundled as a `monoid_hom` when `R` is an `integral_domain`, and thus
   `leading_coeff` is multiplicative -/
 def leading_coeff_hom : polynomial R →* R :=

src/data/polynomial/eval.lean

@@ -103,6 +103,40 @@ begin
   rw [sum_insert, eval₂_add, hs, sum_insert]; assumption,
 end
 
+lemma eval₂_mul_noncomm (hf : ∀ b a, a * f b = f b * a) :
+  (p * q).eval₂ f x = p.eval₂ f x * q.eval₂ f x :=
+begin
+  have f_zero : ∀ (a : ℕ), f 0 * x ^ a = 0,
+  { intro, simp },
+  have f_add : ∀ (a : ℕ) (b₁ b₂ : R), f (b₁ + b₂) * x ^ a = f b₁ * x ^ a + f b₂ * x ^ a,
+  { intros, rw [is_semiring_hom.map_add f, add_mul] },
+
+  simp_rw [eval₂, add_monoid_algebra.mul_def, finsupp.sum_mul _ p, finsupp.mul_sum _ q],
+  rw sum_sum_index; try { assumption },
+  apply sum_congr rfl, assume i hi, dsimp only,
+  rw sum_sum_index; try { assumption },
+  apply sum_congr rfl, assume j hj, dsimp only,
+  rw [sum_single_index, is_semiring_hom.map_mul f, pow_add],
+  { rw [mul_assoc, ←mul_assoc _ (x ^ i), ← hf _ (x ^ i), mul_assoc, mul_assoc] },
+  { apply f_zero }
+ end
+
+lemma eval₂_list_prod_noncomm (ps : list (polynomial R)) (hf : ∀ b a, a * f b = f b * a):
+  ps.prod.eval₂ f x = (ps.map (polynomial.eval₂ f x)).prod :=
+begin
+  induction ps,
+  { simp },
+  { simp [eval₂_mul_noncomm _ _ hf, ps_ih] {contextual := tt} }
+end
+
+/-- `eval₂` as a `ring_hom` for noncommutative rings -/
+def eval₂_ring_hom_noncomm (f : R →+* S) (hf : ∀ b a, a * f b = f b * a) (x : S) : polynomial R →+* S :=
+{ to_fun := eval₂ f x,
+  map_add' := λ _ _, eval₂_add _ _,
+  map_zero' := eval₂_zero _ _,
+  map_mul' := λ _ _, eval₂_mul_noncomm _ _ hf,
+  map_one' := eval₂_one _ _ }
+
 end
 
 /-!
@@ -116,18 +150,8 @@ variables (f : R →+* S) (x : S)
 
 @[simp] lemma eval₂_mul : (p * q).eval₂ f x = p.eval₂ f x * q.eval₂ f x :=
 begin
-  dunfold eval₂,
-  rw [add_monoid_algebra.mul_def, finsupp.sum_mul _ p], simp only [finsupp.mul_sum _ q],
-  rw [sum_sum_index],
-  { apply sum_congr rfl, assume i hi, dsimp only, rw [sum_sum_index],
-    { apply sum_congr rfl, assume j hj, dsimp only,
-      rw [sum_single_index, f.map_mul, pow_add],
-      { simp only [mul_assoc, mul_left_comm] },
-      { rw [f.map_zero, zero_mul] } },
-    { intro, rw [f.map_zero, zero_mul] },
-    { intros, rw [f.map_add, add_mul] } },
-  { intro, rw [f.map_zero, zero_mul] },
-  { intros, rw [f.map_add, add_mul] }
+  apply eval₂_mul_noncomm,
+  simp [mul_comm]
 end
 
 instance eval₂.is_semiring_hom : is_semiring_hom (eval₂ f x) :=
@@ -527,6 +551,15 @@ by apply is_ring_hom.of_semiring
 
 instance eval.is_ring_hom {x : R} : is_ring_hom (eval x) := eval₂.is_ring_hom _
 
+lemma eval₂_endomorphism_algebra_map {M : Type w}
+  [add_comm_group M] [module R M]
+  (f : M →ₗ[R] M) (v : M) (p : polynomial R) :
+  p.eval₂ (algebra_map R (M →ₗ[R] M)) f v = p.sum (λ n b, b • (f ^ n) v) :=
+begin
+  dunfold polynomial.eval₂ finsupp.sum,
+  exact (finset.sum_hom p.support (λ h : M →ₗ[R] M, h v)).symm
+end
+
 end comm_ring
 
 end polynomial

src/data/polynomial/ring_division.lean

@@ -286,6 +286,10 @@ by rw [nat_degree_one, nat_degree_mul hp0 hq0, eq_comm,
   degree (u : polynomial R) = 0 :=
 degree_eq_zero_of_is_unit ⟨u, rfl⟩
 
+lemma units_coeff_zero_smul (c : units (polynomial R)) (p : polynomial R) :
+  (c : polynomial R).coeff 0 • p = c * p :=
+by rw [←polynomial.C_mul', ←polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]
+
 @[simp] lemma nat_degree_coe_units (u : units (polynomial R)) :
   nat_degree (u : polynomial R) = 0 :=
 nat_degree_eq_of_degree_eq_some (degree_coe_units u)