Theorems · Theorem · sequences and series
tsum_eq_zero_of_not_summable
∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
{f : β → α}, ¬Summable f L → ∑'[L] (b : β), f b = 0- Cited by
- 27 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- AddCommMonoidstatement and proof · cited by 12,281
- tsumstatement · cited by 1,148
- Summablestatement and proof · cited by 778
- SummationFilterstatement and proof · cited by 607
- tsum_defproof · cited by 11
Cited by27
Results whose statement or proof uses this declaration.
- tsum_nonnegproof · cited by 18
- Measurable.tsumproof · cited by 8
- tsum_of_norm_boundedproof · cited by 7
- jacobiTheta₂_undefproof · cited by 6
- Topology.IsClosedEmbedding.map_tsumproof · cited by 6
- jacobiTheta₂'_undefproof · cited by 5
- tendsto_tsum_compl_atTop_zeroproof · cited by 3
- NNReal.tsum_eq_toNNReal_tsumproof · cited by 3
- TrivSqZeroExt.exp_def_of_smul_commproof · cited by 3
- cauchySeq_finset_iff_tsum_vanishingproof · cited by 3
- ContinuousMap.periodic_tsum_comp_add_zsmulproof · cited by 2
- differentiable_tsumproof · cited by 2