Theorems · Definition · several complex variables

alternatingGeometricSeries

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

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

Defined in

Mathlib.Analysis.Analytic.Constructions

Cited by

9 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedRingNormedAlgebra