Theorem ModularGroup.exists_one_half_le_im_smul

Modification history

2024-11-20 10:44
Mathlib/NumberTheory/Modular.lean
feat: bounds for modular forms of non-positive weights (#18192) …
Added ModularGroup.exists_one_half_le_im_smulView on Github →