degree_taylor — Mathlib

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]

Похожие утверждения