Theorems · Theorem · sequences and series
summable_nat_add_iff
∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℕ → G} (k : ℕ),
(Summable fun n => f (n + k)) ↔ Summable f- Cited by
- 24 results in Mathlib
- Foundations
- Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- AddCommGroupstatement and proof · cited by 12,871
- Finset.sumproof · cited by 5,195
- SummationFilter.unconditionalstatement · cited by 2,068
- IsTopologicalAddGroupstatement and proof · cited by 1,394
- Finset.rangeproof · cited by 1,341
- Summablestatement · cited by 778
- Equiv.surjectiveproof · cited by 198
- Equiv.addRightproof · cited by 30
- hasSum_nat_add_iffproof · cited by 6
- Function.Surjective.summable_iff_of_hasSum_iffproof · cited by 2
Cited by24
Results whose statement or proof uses this declaration.
- Summable.tsum_eq_zero_addproof · cited by 9
- Summable.sum_add_tsum_nat_addproof · cited by 6
- EisensteinSeries.E_qExpansion_coeffproof · cited by 3
- LiouvilleNumber.remainder_summableproof · cited by 2
- not_summable_of_ratio_norm_eventually_geproof · cited by 2
- AntitoneOn.summable_of_integrableOn_Ioiproof · cited by 2
- ZetaAsymptotics.termTSum_of_ltproof · cited by 2
- NNReal.summable_nat_add_iffproof · cited by 2
- summable_cotTermproof · cited by 2
- ModularForm.multipliableLocallyUniformlyOn_one_sub_powproof · cited by 2
- summable_of_ratio_norm_eventually_leproof · cited by 2
- tendsto_sum_nat_addproof · cited by 2