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