fslope — Mathlib

English

The nth coefficient of fslope(p) equals the (n+1)-st coefficient of p: p.fslope.coeff n = p.coeff (n+1).

Русский

Коэффициент n-ой величины fslope(p) равен коэффициенту (n+1)-й у p: p.fslope.coeff n = p.coeff (n+1).

LaTeX

$$$ p.fslope.coeff n = p.coeff (n+1) $$$

Lean4

/-- The formal counterpart of `dslope`, corresponding to the expansion of `(f z - f 0) / z`. If `f`
has `p` as a power series, then `dslope f` has `fslope p` as a power series. -/
noncomputable def fslope (p : FormalMultilinearSeries 𝕜 𝕜 E) : FormalMultilinearSeries 𝕜 𝕜 E := fun n =>
  (p (n + 1)).curryLeft 1

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