trunc_derivative' — Mathlib

English

For any f and n, trunc (n-1) (d/dX f) = polynomial derivative of trunc n f; with the n=0 case treated separately.

Русский

Для любых f и n: trunc (n-1) (d/dX f) = derivative (trunc n f); при n=0 это тривиально.

LaTeX

$$$ \\operatorname{trunc}_{n-1}\\big( \\tfrac{d}{dX} f \\big) = \\operatorname{derivative}( \\operatorname{trunc}_n f ) \quad( n \\in \\mathbb{N})$$$

Lean4

theorem trunc_derivative' (f : R⟦X⟧) (n : ℕ) : trunc (n - 1) (d⁄dX R f) = Polynomial.derivative (trunc n f) := by
  cases n with
  | zero => simp
  | succ n => rw [succ_sub_one, trunc_derivative]

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