chore(data/polynomial/derivative): use 'nat_cast' rather than 'cast_n…

…at' for consistency (#16005)
leanprover-community · Aug 11, 2022 · acae0c3 · acae0c3
1 parent fc32854
commit acae0c3
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/src/data/polynomial/derivative.lean b/src/data/polynomial/derivative.lean
@@ -158,7 +158,7 @@ begin
   { exact nat.le_pred_of_lt (nat_degree_derivative_lt p0) }
 end
 
-@[simp] lemma derivative_cast_nat {n : ℕ} : derivative (n : R[X]) = 0 :=
+@[simp] lemma derivative_nat_cast {n : ℕ} : derivative (n : R[X]) = 0 :=
 begin
   rw ← map_nat_cast C n,
   exact derivative_C,
@@ -248,7 +248,7 @@ begin
   { simp only [ih, function.iterate_succ, polynomial.derivative_map, function.comp_app], },
 end
 
-@[simp] lemma iterate_derivative_cast_nat_mul {n k : ℕ} {f : R[X]} :
+@[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*
 

diff --git a/src/ring_theory/polynomial/bernstein.lean b/src/ring_theory/polynomial/bernstein.lean
@@ -153,7 +153,7 @@ begin
     { simp [eval_at_0], },
     { simp only [derivative_succ, int.coe_nat_eq_zero, mul_eq_zero,
         function.comp_app, function.iterate_succ,
-        polynomial.iterate_derivative_sub, polynomial.iterate_derivative_cast_nat_mul,
+        polynomial.iterate_derivative_sub, polynomial.iterate_derivative_nat_cast_mul,
         polynomial.eval_mul, polynomial.eval_nat_cast, polynomial.eval_sub],
       intro h,
       apply mul_eq_zero_of_right,
@@ -180,7 +180,7 @@ begin
     { have h' : ν ≤ n-1 := le_tsub_of_add_le_right h,
       simp only [derivative_succ, ih (n-1) h', iterate_derivative_succ_at_0_eq_zero,
         nat.succ_sub_succ_eq_sub, tsub_zero, sub_zero,
-        iterate_derivative_sub, iterate_derivative_cast_nat_mul,
+        iterate_derivative_sub, iterate_derivative_nat_cast_mul,
         eval_one, eval_mul, eval_add, eval_sub, eval_X, eval_comp, eval_nat_cast,
         function.comp_app, function.iterate_succ, pochhammer_succ_left],
       obtain rfl | h'' := ν.eq_zero_or_pos,