derivative_apply — Mathlib

English

For every Laurent series f, the derivative is the first Hasse derivative applied to f: derivative(R) f = hasseDeriv(R,1) f.

Русский

Для любой Лаурентовой серии f производная равна первой производной Хассе: derivative(R) f = hasseDeriv(R,1) f.

LaTeX

$$$\mathrm{derivative}(R)\, f = \mathrm{hasseDeriv}(R,1)\, f$$$

Lean4

@[simp]
theorem derivative_apply (f : LaurentSeries V) : derivative R f = hasseDeriv R 1 f := by exact rfl

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