English
Adding a zeroth term z to a formal multilinear series q producing a new p means p(0) = (curryFin0)^{-1}(z) and p(n+1) = (q n) under a suitable curry equivalence.
Русский
Добавление нулевого члена z к формальному мультилинейному ряду q даёт новый p; нулевой член определяется обратной степенью карриFin0, а остальные члены задаются через q через эквивалентности карри.
LaTeX
$$$\\text{unshift}\\, (q)\\, z\\;:\\; p(0) = (\\text{curryFin0}\\, 𝕜\\, E\\, F)^{-1} z,\\; p(n+1) = (q\\, n)$$$
Lean4
/-- Adding a zeroth term to a formal multilinear series taking values in `E →L[𝕜] F`. This
corresponds to starting from a Taylor series (`HasFTaylorSeriesUpTo`) for the derivative of a
function, and building a Taylor series for the function itself. -/
def unshift (q : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)) (z : F) : FormalMultilinearSeries 𝕜 E F
| 0 => (continuousMultilinearCurryFin0 𝕜 E F).symm z
| n + 1 => (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm (q n)
