toFormalMultilinearSeries — Mathlib

English

At the level of values, (f.compFormalMultilinearSeries p)(n) evaluated at v equals f(p(n) v).

Русский

На уровне значений: (f.compFormalMultilinearSeries p)(n)(v) = f(p(n)(v)).

LaTeX

$$$(f.compFormalMultilinearSeries p)(n)(v) = f\\big(p(n)(v)\\big)$$$

Lean4

/-- Realize a ContinuousMultilinearMap on `∀ i : ι, E i` as the evaluation of a
FormalMultilinearSeries by choosing an arbitrary identification `ι ≃ Fin (Fintype.card ι)`. -/
noncomputable def toFormalMultilinearSeries : FormalMultilinearSeries 𝕜 (∀ i, E i) F := fun n ↦
  if h : Fintype.card ι = n then (f.compContinuousLinearMap .proj).domDomCongr (Fintype.equivFinOfCardEq h) else 0

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