Theorems · Theorem · commutative algebra

PowerSeries.hasSum_of_monomials_self

∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] (f : PowerSeries R),
  HasSum (fun d => (PowerSeries.monomial d) ((PowerSeries.coeff d) f)) f

A power series is the sum (in the sense of summable families) of its monomials

Defined in

Mathlib.RingTheory.PowerSeries.PiTopology

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringTopologicalSpace