Theorems · Theorem · number theory
EisensteinSeries.summable_linear_right_add_one_mul_linear_right
∀ (z : ℂ) (c₁ c₂ : ℤ), Summable fun n => ((↑c₁ * z + ↑n + 1) * (↑c₂ * z + ↑n))⁻¹
- 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.
- 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_oneproof · cited by 371
- mul_inv_revproof · cited by 270
- pow_twoproof · cited by 150
- Asymptotics.IsBigO.mulproof · cited by 29
- abs_mul_abs_selfproof · cited by 21
- Real.rpow_ofNatproof · cited by 12
Cited by1
Results whose statement or proof uses this declaration.
- EisensteinSeries.summable_right_one_div_linear_sub_one_div_linear_succproof · cited by 0