compFormalMultilinearSeries — Mathlib

English

The order of a formal multilinear series p is defined as the least index n with p(n) ≠ 0, i.e., p.order = inf { n | p(n) ≠ 0 }. If all terms vanish, the order is 0 by definition.

Русский

Порядок формального мультилинейного ряда p — наименьшее n такое, что p(n) ≠ 0 (или 0, если все члены равны нулю).

LaTeX

$$$\\operatorname{order}(p) = \\inf\\{n \\mid p(n) \\neq 0\\}$$$

Lean4

/-- Composing each term `pₙ` in a formal multilinear series with a continuous linear map `f` on the
left gives a new formal multilinear series `f.compFormalMultilinearSeries p` whose general term
is `f ∘ pₙ`. -/
def compFormalMultilinearSeries (f : F →L[𝕜] G) (p : FormalMultilinearSeries 𝕜 E F) : FormalMultilinearSeries 𝕜 E G :=
  fun n => f.compContinuousMultilinearMap (p n)

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