chore(data/polynomial/derivative): change n to C n (#17795)

For convenience and for consistency with the `derivative_C_mul_X_pow` lemmas.

src/data/polynomial/derivative.lean

@@ -81,10 +81,10 @@ by rw [C_mul_X_pow_eq_monomial, C_mul_X_pow_eq_monomial, derivative_monomial]
 lemma derivative_C_mul_X_sq (a : R) : derivative (C a * X ^ 2) = C (a * 2) * X :=
 by rw [derivative_C_mul_X_pow, nat.cast_two, pow_one]
 
-@[simp] lemma derivative_X_pow (n : ℕ) : derivative (X ^ n : R[X]) = (n : R[X]) * X ^ (n - 1) :=
+@[simp] lemma derivative_X_pow (n : ℕ) : derivative (X ^ n : R[X]) = C ↑n * X ^ (n - 1) :=
 by convert derivative_C_mul_X_pow (1 : R) n; simp
 
-@[simp] lemma derivative_X_sq : derivative (X ^ 2 : R[X]) = (2 : R[X]) * X :=
+@[simp] lemma derivative_X_sq : derivative (X ^ 2 : R[X]) = C 2 * X :=
 by rw [derivative_X_pow, nat.cast_two, pow_one]
 
 @[simp] lemma derivative_C {a : R} : derivative (C a) = 0 :=
@@ -105,8 +105,7 @@ by simp [bit0]
 @[simp] lemma derivative_bit1 {a : R[X]} : derivative (bit1 a) = bit0 (derivative a) :=
 by simp [bit1]
 
-@[simp] lemma derivative_add {f g : R[X]} :
-  derivative (f + g) = derivative f + derivative g :=
+@[simp] lemma derivative_add {f g : R[X]} : derivative (f + g) = derivative f + derivative g :=
 derivative.map_add f g
 
 @[simp] lemma iterate_derivative_add {f g : R[X]} {k : ℕ} :
@@ -416,17 +415,17 @@ lemma iterate_derivative_X_pow_eq_nat_cast_mul (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,
+  { rw [function.iterate_succ_apply', ih, derivative_nat_cast_mul, derivative_X_pow, C_eq_nat_cast,
       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) :=
+  (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) :=
+  (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) :=

src/field_theory/finite/basic.lean

@@ -264,8 +264,8 @@ begin
   apply nodup_roots,
   rw separable_def,
   convert is_coprime_one_right.neg_right using 1,
-  { rw [derivative_sub, derivative_X, derivative_X_pow, ←C_eq_nat_cast,
-    C_eq_zero.mpr (char_p.cast_card_eq_zero K), zero_mul, zero_sub], },
+  { rw [derivative_sub, derivative_X, derivative_X_pow, char_p.cast_card_eq_zero K, C_0, zero_mul,
+      zero_sub] },
   end
 
 instance (F : Type*) [field F] [algebra F K] : is_splitting_field F K (X^q - X) :=

src/field_theory/separable.lean

@@ -365,9 +365,8 @@ begin
   rw [separable_def', derivative_sub, derivative_X_pow, derivative_one, sub_zero],
   -- Suppose `(n : F) = 0`, then the derivative is `0`, so `X ^ n - 1` is a unit, contradiction.
   rintro (h : is_coprime _ _) hn',
-  rw [← C_eq_nat_cast, hn', C.map_zero, zero_mul, is_coprime_zero_right] at h,
-  have := not_is_unit_X_pow_sub_one F n,
-  contradiction
+  rw [hn', C_0, zero_mul, is_coprime_zero_right] at h,
+  exact not_is_unit_X_pow_sub_one F n h
 end
 
 section splits

src/ring_theory/polynomial/chebyshev.lean

@@ -185,10 +185,10 @@ begin
   have h : derivative (T R (n + 2)) = (U R (n + 1) - X * U R n) + X * derivative (T R (n + 1))
                                       + 2 * X * U R n - (1 - X ^ 2) * derivative (U R n),
   { conv_lhs { rw T_eq_X_mul_T_sub_pol_U },
-  simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow,
-  one_mul, T_derivative_eq_U],
-  rw [T_eq_U_sub_X_mul_U, nat.cast_bit0, nat.cast_one],
-  ring },
+    simp only [derivative_sub, derivative_mul, derivative_X, derivative_one, derivative_X_pow,
+              one_mul, T_derivative_eq_U],
+    rw [T_eq_U_sub_X_mul_U, C_eq_nat_cast, nat.cast_bit0, nat.cast_one],
+    ring },
   calc ((n : R[X]) + 1) * T R (n + 1)
       = ((n : R[X]) + 1 + 1) * (X * U R n + T R (n + 1))
         - X * ((n + 1) * U R n) - (X * U R n + T R (n + 1)) : by ring