Theorems · Definition · several complex variables

formalMultilinearSeries_geometric

(𝕜 : Type u_2) →
  [inst : NontriviallyNormedField 𝕜] →
    (A : Type u_7) → [inst_1 : NormedRing A] → [inst_2 : NormedAlgebra 𝕜 A] → FormalMultilinearSeries 𝕜 A A

The geometric series 1 + x + x ^ 2 + ... as a FormalMultilinearSeries.

Defined in

Mathlib.Analysis.Analytic.Constructions

Cited by

12 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedRingNormedAlgebra