Theorems · Theorem · number theory
EisensteinSeries.linear_left_summable
∀ {z : ℂ}, z ≠ 0 → ∀ (d : ℤ) {k : ℤ}, 2 ≤ k → Summable fun c => ((↑c * z + ↑d) ^ k)⁻¹For z : ℂ the function c : ℤ ↦ ((c z + d) ^ k)⁻¹ is Summable for 2 ≤ k.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realproof · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Nat.cast_oneproof · cited by 2,501
- SummationFilter.unconditionalstatement · cited by 2,068
- absproof · cited by 1,814
- Summablestatement · cited by 778
- Asymptotics.IsBigOproof · cited by 506
- Int.cast_natCastproof · cited by 393
- Int.cast_oneproof · cited by 371
- zpow_natCastproof · cited by 271
- Filter.cofiniteproof · cited by 251
- Real.rpow_natCastproof · cited by 93
Cited by1
Results whose statement or proof uses this declaration.
- EisensteinSeries.tsum_symmetricIco_tsum_eq_S_actproof · cited by 0