Theorem UpperHalfPlane.im_pnat_div_pos

Modification history

2025-12-27 18:03

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

feat(NumberTheory/ModularForms/EisensteinSeries/Summable): add auxiliary E2 lemmas (#32955) …

Added UpperHalfPlane.im_pnat_div_pos View on Github →