Theorems · Theorem · number theory
EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act
∀ (z : UpperHalfPlane),
∑'[SummationFilter.symmetricIco ℤ] (n : ℤ), ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2 =
(↑z ^ 2)⁻¹ * EisensteinSeries.G2 (ModularGroup.S • z)- Cited by
- 0 results in Mathlib
- Foundations
- Depth 315 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites23
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Finset.sumproof · cited by 5,195
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- le_rflproof · cited by 1,558
- tsumstatement and proof · cited by 1,148
- Summableproof · cited by 778
- UpperHalfPlanestatement and proof · cited by 626
- one_divproof · cited by 624
- Finset.Icoproof · cited by 450
- Matrix.SpecialLinearGroupstatement · cited by 348
- UpperHalfPlane.coestatement and proof · cited by 288
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.