feat(data/polynomial/derivative): add more lemmas (#16139)

Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>

src/data/polynomial/derivative.lean

@@ -257,6 +257,10 @@ begin
   { simp only [ih, function.iterate_succ, polynomial.derivative_map, function.comp_app], },
 end
 
+lemma derivative_nat_cast_mul {n : ℕ} {f : R[X]} :
+  (↑n * f).derivative = n * f.derivative :=
+by simp
+
 @[simp] lemma iterate_derivative_nat_cast_mul {n k : ℕ} {f : R[X]} :
   derivative^[k] (n * f) = n * (derivative^[k] f) :=
 by induction k with k ih generalizing f; simp*
@@ -386,6 +390,48 @@ theorem derivative_pow (p : R[X]) (n : ℕ) :
 nat.cases_on n (by rw [pow_zero, derivative_one, nat.cast_zero, zero_mul, zero_mul]) $ λ n,
 by rw [p.derivative_pow_succ n, n.succ_sub_one, n.cast_succ]
 
+theorem dvd_iterate_derivative_pow (f : R[X]) (n : ℕ) {m : ℕ} (c : R) (hm : m ≠ 0) :
+  (n : R) ∣ eval c (derivative^[m] (f ^ n)) :=
+begin
+  obtain ⟨m, rfl⟩ := nat.exists_eq_succ_of_ne_zero hm,
+  rw [function.iterate_succ_apply, derivative_pow, mul_assoc, iterate_derivative_nat_cast_mul,
+    eval_mul, eval_nat_cast],
+  exact dvd_mul_right _ _,
+end
+
+lemma iterate_derivative_X_pow_eq_nat_cast_mul (n k : ℕ) :
+  (derivative^[k] (X ^ n : R[X])) = ↑(nat.desc_factorial n k) * X ^ (n - k) :=
+begin
+  induction k with k ih,
+  { rw [function.iterate_zero_apply, tsub_zero, nat.desc_factorial_zero, nat.cast_one, one_mul] },
+  { rw [function.iterate_succ_apply', ih, derivative_nat_cast_mul, derivative_X_pow,
+      nat.succ_eq_add_one, nat.desc_factorial_succ, nat.sub_sub, nat.cast_mul, ←mul_assoc,
+      mul_comm ↑(nat.desc_factorial _ _)] },
+end
+
+lemma iterate_derivative_X_pow_eq_C_mul (n k : ℕ) :
+  (derivative^[k] (X^n : R[X])) = C ↑(nat.desc_factorial n k) * X ^ (n - k) :=
+by rw [iterate_derivative_X_pow_eq_nat_cast_mul n k, C_eq_nat_cast]
+
+lemma iterate_derivative_X_pow_eq_smul (n : ℕ) (k : ℕ) :
+  (derivative^[k] (X^n : R[X])) = (nat.desc_factorial n k : R) • X ^ (n - k) :=
+by rw [iterate_derivative_X_pow_eq_C_mul n k, smul_eq_C_mul]
+
+lemma derivative_X_add_pow (c : R) (m : ℕ) : ((X + C c) ^ m).derivative = m * (X + C c) ^ (m - 1) :=
+by rw [derivative_pow, derivative_add, derivative_X, derivative_C, add_zero, mul_one]
+
+lemma iterate_derivative_X_add_pow (n k : ℕ) (c : R) :
+  (derivative^[k] ((X + C c) ^ n)) =
+  ↑(∏ i in finset.range k, (n - i)) * (X + C c) ^ (n - k) :=
+begin
+  induction k with k IH,
+  { rw [function.iterate_zero_apply, finset.range_zero, finset.prod_empty, nat.cast_one, one_mul,
+      tsub_zero] },
+  { simp only [function.iterate_succ_apply', IH, derivative_mul, zero_mul, derivative_nat_cast,
+      zero_add, finset.prod_range_succ, C_eq_nat_cast, nat.sub_sub, ←mul_assoc,
+      derivative_X_add_pow, nat.succ_eq_add_one, nat.cast_mul] },
+end
+
 lemma derivative_comp (p q : R[X]) :
   (p.comp q).derivative = q.derivative * p.derivative.comp q :=
 begin
@@ -448,6 +494,20 @@ linear_map.map_sub derivative f g
   derivative^[k] (f - g) = (derivative^[k] f) - (derivative^[k] g) :=
 by induction k with k ih generalizing f g; simp*
 
+@[simp] lemma derivative_int_cast {n : ℤ} : derivative (n : R[X]) = 0 :=
+begin
+  rw ← C_eq_int_cast n,
+  exact derivative_C,
+end
+
+lemma derivative_int_cast_mul {n : ℤ} {f : R[X]} :
+  (↑n * f).derivative = n * f.derivative :=
+by simp
+
+@[simp] lemma iterate_derivative_int_cast_mul {n : ℤ} {k : ℕ} {f : R[X]} :
+  derivative^[k] (↑n * f) = n * (derivative^[k] f) :=
+by induction k with k ih generalizing f; simp*
+
 end ring
 
 section comm_ring
@@ -474,6 +534,15 @@ begin
   simpa using (eval_ring_hom r).map_multiset_prod (multiset.map (λ a, X - C a) (S.erase r)),
 end
 
+lemma derivative_X_sub_pow (c : R) (m : ℕ) :
+  ((X - C c) ^ m).derivative = m * (X - C c) ^ (m - 1) :=
+by rw [derivative_pow, derivative_sub, derivative_X, derivative_C, sub_zero, mul_one]
+
+lemma iterate_derivative_X_sub_pow (n k : ℕ) (c : R) :
+  (derivative^[k] ((X - C c) ^ n)) =
+  (↑(∏ i in finset.range k, (n - i))) * (X - C c) ^ (n - k) :=
+by simp_rw [sub_eq_add_neg, ←C_neg, iterate_derivative_X_add_pow]
+
 end comm_ring
 
 end derivative