English
Derivative of a natural number cast to polynomials is zero.
Русский
Производная натурального числа, превращенного в полиномы, равна нулю.
LaTeX
$$$\operatorname{derivative}(n) = 0$$$
Lean4
@[simp]
theorem derivative_map [Semiring S] (p : R[X]) (f : R →+* S) : derivative (p.map f) = p.derivative.map f :=
by
let n := max p.natDegree (map f p).natDegree
rw [derivative_apply, derivative_apply]
rw [sum_over_range' _ _ (n + 1) ((le_max_left _ _).trans_lt (lt_add_one _))]
on_goal 1 => rw [sum_over_range' _ _ (n + 1) ((le_max_right _ _).trans_lt (lt_add_one _))]
·
simp only [Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_C, map_mul, coeff_map, map_natCast,
Polynomial.map_natCast, Polynomial.map_pow, map_X]
all_goals intro n; rw [zero_mul, C_0, zero_mul]
