taylor_apply — Mathlib

English

There exists gp with bounds and a relation expressing aeval of sumIDeriv in terms of aeval of gp for all r, covering various divisibility scenarios.

Русский

Существует gp с ограничениями по степени и соотношение, выражающее aeval(sumIDeriv p) через aeval gp при всех r и для различных сценариев делимости.

LaTeX

$$$$ \exists gp ∈ R[X], \; \operatorname{natDegree}(gp) ≤ \operatorname{natDegree}(p) - q \; \wedge\; \forall r, (X - C r)^q \mid p.map(algebraMap R A) \Rightarrow \cdot \cdot \Rightarrow \text{усл.} $$$$

Lean4

theorem taylor_apply : taylor r f = f.comp (X + C r) :=
  rfl

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