Theorems · Theorem · sequences and series

summable_finset_prod_of_summable_norm

Deprecated since 2026-04-08Use summable_finsetProd_of_summable_norm instead.

∀ {ι : Type u_1} {R : Type u_2} [inst : NormedCommRing R] [NormOneClass R] {f : ι → R} [CompleteSpace R],
  (Summable fun i => ‖f i‖) → Summable fun s => ∏ i ∈ s, f i

Alias of summable_finsetProd_of_summable_norm.

Defined in

Mathlib.Analysis.SpecialFunctions.Log.Summable

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedCommRingNormOneClassCompleteSpace