Theorems · Definition · sequences and series

Multipliable

{α : Type u_1} →
  {β : Type u_2} →
    [CommMonoid α] →
      [TopologicalSpace α] → (β → α) → optParam (SummationFilter β) (SummationFilter.unconditional β) → Prop

Multipliable f means that f has some (infinite) product with respect to L. Use tprod to get the value.

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Defs

Cited by

213 results in Mathlib

Foundations

Depth 57 from the axioms, rests on 924 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidTopologicalSpace