Theorems · Definition · functional analysis

FormalMultilinearSeries.coeff

{𝕜 : Type u} →
  {E : Type v} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → FormalMultilinearSeries 𝕜 𝕜 E → ℕ → E

The nth coefficient of p when seen as a power series.

Defined in

Mathlib.Analysis.Calculus.FormalMultilinearSeries

Cited by

30 results in Mathlib

Foundations

Depth 167 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace