English
For any polynomial p ∈ R[X] and any r ∈ R, the degree of the Taylor expansion taylor(r,p) equals the degree of p.
Русский
Для любого полинома p ∈ R[X] и любого r ∈ R степень полинома taylor(r,p) равна степени p.
LaTeX
$$$$ \\deg(\\operatorname{taylor}(r,p)) = \\deg(p). $$$$
Lean4
@[simp]
theorem degree_taylor (p : R[X]) (r : R) : degree (taylor r p) = degree p :=
by
by_cases hp : p = 0
· rw [hp, map_zero]
· rw [degree_eq_natDegree hp, degree_eq_iff_natDegree_eq ((taylor_eq_zero r p).not.2 hp), natDegree_taylor]