Theorems · Theorem · number theory
summable_prod_mul_pow
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormSMulClass ℤ 𝕜] (k : ℕ) {r : 𝕜},
‖r‖ < 1 → Summable fun c => ↑↑c.2 ^ k * r ^ (↑c.1 * ↑c.2)- Cited by
- 2 results in Mathlib
- Foundations
- Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- TopologicalSpaceproof · cited by 24,529
- AddCommMonoidproof · cited by 12,281
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- Norm.normstatement and proof · cited by 5,413
- CompleteSpacestatement and proof · cited by 2,532
- SummationFilter.unconditionalstatement · cited by 2,068
- Summablestatement · cited by 778
- PNatstatement and proof · cited by 392
- PNat.valstatement and proof · cited by 226
- NormSMulClassstatement and proof · cited by 107
- Equiv.summable_iffproof · cited by 17
Cited by2
Results whose statement or proof uses this declaration.
- tsum_prod_pow_eq_tsum_sigmaproof · cited by 2
- tsum_pow_div_one_sub_eq_tsum_sigmaproof · cited by 1