chore(data/polynomial/derivative): replace n by C n (#17911)

Rename `derivative_pow` lemmas, refactor `derivative_X_add_pow` slightly, and replace `n` by `C n` analogously to #17795

Author: Multramate

src/data/polynomial/derivative.lean

@@ -108,6 +108,9 @@ by simp [bit1]
 @[simp] lemma derivative_add {f g : R[X]} : derivative (f + g) = derivative f + derivative g :=
 derivative.map_add f g
 
+@[simp] lemma derivative_X_add_C (c : R) : (X + C c).derivative = 1 :=
+by rw [derivative_add, derivative_X, derivative_C, add_zero]
+
 @[simp] lemma iterate_derivative_add {f g : R[X]} {k : ℕ} :
   derivative^[k] (f + g) = (derivative^[k] f) + (derivative^[k] g) :=
 derivative.to_add_monoid_hom.iterate_map_add _ _ _
@@ -391,22 +394,25 @@ section comm_semiring
 variables [comm_semiring R]
 
 theorem derivative_pow_succ (p : R[X]) (n : ℕ) :
-  (p ^ (n + 1)).derivative = (n + 1) * (p ^ n) * p.derivative :=
-nat.rec_on n (by rw [pow_one, nat.cast_zero, zero_add, one_mul, pow_zero, one_mul]) $ λ n ih,
-by rw [pow_succ', derivative_mul, ih, mul_right_comm, ← add_mul,
-    add_mul (n.succ : R[X]), one_mul, pow_succ', mul_assoc, n.cast_succ]
+  (p ^ (n + 1)).derivative = C ↑(n + 1) * (p ^ n) * p.derivative :=
+nat.rec_on n (by rw [pow_one, nat.cast_one, C_1, one_mul, pow_zero, one_mul]) $ λ n ih,
+by rw [pow_succ', derivative_mul, ih, nat.add_one, mul_right_comm, nat.cast_add n.succ, C_add,
+       add_mul, add_mul, pow_succ', ← mul_assoc, nat.cast_one, C_1, one_mul]
 
 theorem derivative_pow (p : R[X]) (n : ℕ) :
-  (p ^ n).derivative = n * (p ^ (n - 1)) * p.derivative :=
-nat.cases_on n (by rw [pow_zero, derivative_one, nat.cast_zero, zero_mul, zero_mul]) $ λ n,
+  (p ^ n).derivative = C ↑n * (p ^ (n - 1)) * p.derivative :=
+nat.cases_on n (by rw [pow_zero, derivative_one, nat.cast_zero, C_0, zero_mul, zero_mul]) $ λ n,
 by rw [p.derivative_pow_succ n, n.succ_sub_one, n.cast_succ]
 
+theorem derivative_sq (p : R[X]) : (p ^ 2).derivative = C 2 * p * p.derivative :=
+by rw [derivative_pow_succ, nat.cast_two, pow_one]
+
 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],
+  rw [function.iterate_succ_apply, derivative_pow, mul_assoc, C_eq_nat_cast,
+      iterate_derivative_nat_cast_mul, eval_mul, eval_nat_cast],
   exact dvd_mul_right _ _,
 end
 
@@ -428,23 +434,25 @@ 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 derivative_X_add_C_pow (c : R) (m : ℕ) :
+  ((X + C c) ^ m).derivative = C ↑m * (X + C c) ^ (m - 1) :=
+by rw [derivative_pow, derivative_X_add_C, mul_one]
+
+lemma derivative_X_add_C_sq (c : R) : ((X + C c) ^ 2).derivative = C 2 * (X + C c) :=
+by rw [derivative_sq, derivative_X_add_C, mul_one]
 
-lemma iterate_derivative_X_add_pow (n k : ℕ) (c : R) :
-  (derivative^[k] ((X + C c) ^ n)) =
+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] },
+      derivative_X_add_C_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 :=
+lemma derivative_comp (p q : R[X]) : (p.comp q).derivative = q.derivative * p.derivative.comp q :=
 begin
   apply polynomial.induction_on' p,
   { intros p₁ p₂ h₁ h₂, simp [h₁, h₂, mul_add], },
@@ -497,10 +505,12 @@ linear_map.map_neg derivative f
   derivative^[k] (-f) = - (derivative^[k] f) :=
 (@derivative R _).to_add_monoid_hom.iterate_map_neg _ _
 
-@[simp] lemma derivative_sub {f g : R[X]} :
-  derivative (f - g) = derivative f - derivative g :=
+@[simp] lemma derivative_sub {f g : R[X]} : derivative (f - g) = derivative f - derivative g :=
 linear_map.map_sub derivative f g
 
+@[simp] lemma derivative_X_sub_C (c : R) : (X - C c).derivative = 1 :=
+by rw [derivative_sub, derivative_X, derivative_C, sub_zero]
+
 @[simp] lemma iterate_derivative_sub {k : ℕ} {f g : R[X]} :
   derivative^[k] (f - g) = (derivative^[k] f) - (derivative^[k] g) :=
 by induction k with k ih generalizing f g; simp*
@@ -525,12 +535,12 @@ section comm_ring
 variables [comm_ring R]
 
 lemma derivative_comp_one_sub_X (p : R[X]) :
-  (p.comp (1-X)).derivative = -p.derivative.comp (1-X) :=
+  (p.comp (1 - X)).derivative = -p.derivative.comp (1 - X) :=
 by simp [derivative_comp]
 
 @[simp]
 lemma iterate_derivative_comp_one_sub_X (p : R[X]) (k : ℕ) :
-  derivative^[k] (p.comp (1-X)) = (-1)^k * (derivative^[k] p).comp (1-X) :=
+  derivative^[k] (p.comp (1 - X)) = (-1) ^ k * (derivative^[k] p).comp (1 - X) :=
 begin
   induction k with k ih generalizing p,
   { simp, },
@@ -545,16 +555,19 @@ 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 derivative_X_sub_C_pow (c : R) (m : ℕ) :
+  ((X - C c) ^ m).derivative = C ↑m * (X - C c) ^ (m - 1) :=
+by rw [derivative_pow, derivative_X_sub_C, mul_one]
+
+lemma derivative_X_sub_C_sq (c : R) : ((X - C c) ^ 2).derivative = C 2 * (X - C c) :=
+by rw [derivative_sq, derivative_X_sub_C, 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) :=
+  (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
+
 end polynomial

src/data/polynomial/expand.lean

@@ -70,7 +70,7 @@ by rw [function.iterate_succ_apply', pow_succ, expand_mul, ih]
 
 theorem derivative_expand (f : R[X]) :
   (expand R p f).derivative = expand R p f.derivative * (p * X ^ (p - 1)) :=
-by rw [coe_expand, derivative_eval₂_C, derivative_pow, derivative_X, mul_one]
+by rw [coe_expand, derivative_eval₂_C, derivative_pow, C_eq_nat_cast, derivative_X, mul_one]
 
 theorem coeff_expand {p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) :
   (expand R p f).coeff n = if p ∣ n then f.coeff (n / p) else 0 :=

src/data/polynomial/field_division.lean

@@ -36,12 +36,12 @@ begin
   have hn : n + 1 = _ := tsub_add_cancel_of_le ((root_multiplicity_pos hp).mpr hpt),
   rw ←hn,
   set q := p /ₘ (X - C t) ^ (n + 1) with hq,
-  convert_to root_multiplicity t ((X - C t) ^ n * (derivative q * (X - C t) + q * ↑(n + 1))) = n,
+  convert_to root_multiplicity t ((X - C t) ^ n * (derivative q * (X - C t) + q * C ↑(n + 1))) = n,
   { congr,
     rw [mul_add, mul_left_comm $ (X - C t) ^ n, ←pow_succ'],
     congr' 1,
     rw [mul_left_comm $ (X - C t) ^ n, mul_comm $ (X - C t) ^ n] },
-  have h : (derivative q * (X - C t) + q * ↑(n + 1)).eval t ≠ 0,
+  have h : (derivative q * (X - C t) + q * C ↑(n + 1)).eval t ≠ 0,
   { suffices : eval t q * ↑(n + 1) ≠ 0,
     { simpa },
     refine mul_ne_zero _ (nat.cast_ne_zero.mpr n.succ_ne_zero),

src/field_theory/finite/galois_field.lean

@@ -38,7 +38,7 @@ lemma galois_poly_separable {K : Type*} [field K] (p q : ℕ) [char_p K p] (h :
 begin
   use [1, (X ^ q - X - 1)],
   rw [← char_p.cast_eq_zero_iff K[X] p] at h,
-  rw [derivative_sub, derivative_pow, derivative_X, h],
+  rw [derivative_sub, derivative_X_pow, derivative_X, C_eq_nat_cast, h],
   ring,
 end
 

src/number_theory/cyclotomic/discriminant.lean

@@ -103,9 +103,9 @@ begin
         hp.out.one_lt) (pow_pos hp.out.pos _))) (even.mul_right (nat.even_sub_one_of_prime_ne_two
         hp.out hptwo) _) odd_one) } },
   { have H := congr_arg derivative (cyclotomic_prime_pow_mul_X_pow_sub_one K p k),
-    rw [derivative_mul, derivative_sub, derivative_one, sub_zero, derivative_pow,
-      derivative_X, mul_one, derivative_sub, derivative_one, sub_zero, derivative_pow,
-      derivative_X, mul_one, ← pnat.pow_coe, hζ.minpoly_eq_cyclotomic_of_irreducible hirr] at H,
+    rw [derivative_mul, derivative_sub, derivative_one, sub_zero, derivative_X_pow, C_eq_nat_cast,
+      derivative_sub, derivative_one, sub_zero, derivative_X_pow, C_eq_nat_cast, ← pnat.pow_coe,
+      hζ.minpoly_eq_cyclotomic_of_irreducible hirr] at H,
     replace H := congr_arg (λ P, aeval ζ P) H,
     simp only [aeval_add, aeval_mul, minpoly.aeval, zero_mul, add_zero, aeval_nat_cast,
       _root_.map_sub, aeval_one, aeval_X_pow] at H,

src/ring_theory/polynomial/bernstein.lean

@@ -98,14 +98,15 @@ lemma derivative_succ_aux (n ν : ℕ) :
 begin
   rw [bernstein_polynomial],
   suffices :
-    ↑((n + 1).choose (ν + 1)) * ((↑ν + 1) * X ^ ν) * (1 - X) ^ (n - ν)
+    ↑((n + 1).choose (ν + 1)) * (↑(ν + 1) * X ^ ν) * (1 - X) ^ (n - ν)
       -(↑((n + 1).choose (ν + 1)) * X ^ (ν + 1) * (↑(n - ν) * (1 - X) ^ (n - ν - 1))) =
-    (↑n + 1) * (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν) -
+    ↑(n + 1) * (↑(n.choose ν) * X ^ ν * (1 - X) ^ (n - ν) -
          ↑(n.choose (ν + 1)) * X ^ (ν + 1) * (1 - X) ^ (n - (ν + 1))),
   { simpa only [polynomial.derivative_pow, ←sub_eq_add_neg, nat.succ_sub_succ_eq_sub,
       polynomial.derivative_mul, polynomial.derivative_nat_cast, zero_mul, nat.cast_add,
       algebra_map.coe_one, polynomial.derivative_X, mul_one, zero_add,
-      polynomial.derivative_sub, polynomial.derivative_one, zero_sub, mul_neg] },
+      polynomial.derivative_sub, polynomial.derivative_one, zero_sub, mul_neg,
+      nat.sub_zero, ← nat.cast_succ, polynomial.C_eq_nat_cast], },
   conv_rhs { rw mul_sub, },
   -- We'll prove the two terms match up separately.
   refine congr (congr_arg has_sub.sub _) _,