derivative — Mathlib

English

The formal derivative is defined as a derivation from the power-series ring to itself, satisfying linearity and Leibniz rule.

Русский

Формальная производная определяется как производная из кольца степенных рядов в себя, удовлетворяющая линейности и правилу Лейбница.

LaTeX

$$$ \\text{PowerSeries.derivative} : \\text{Derivation } R \\; (\\mathbb{R}[[X]]) \\to \\mathbb{R}[[X]] $$$

Lean4

/-- The formal derivative of a formal power series -/
noncomputable def derivative : Derivation R R⟦X⟧ R⟦X⟧
    where
  toFun := derivativeFun
  map_add' := derivativeFun_add
  map_smul' := derivativeFun_smul
  map_one_eq_zero' := derivativeFun_one
  leibniz' := derivativeFun_mul

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