trunc_derivative

Mathlib.RingTheory.PowerSeries.Derivative

URI: https://scilib.ai/kg/mathlib#PowerSeries.trunc_derivative

English

For a power-series f and n, trunc n (d/dX f) equals the derivative of trunc (n+1) f.

Русский

Для степенного ряда f и n: trunc n (d/dX f) = derivative (trunc (n+1) f).

LaTeX

$$$ \\operatorname{trunc}_n\\big( \\frac{d}{dX} f \\big) = \\operatorname{derivative}( \\operatorname{trunc}_{n+1} f )$$$

Lean4

theorem trunc_derivative (f : R⟦X⟧) (n : ℕ) : trunc n (d⁄dX R f) = Polynomial.derivative (trunc (n + 1) f) :=
  trunc_derivativeFun ..

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru