Theorem ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le

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_smul_and_norm_denom_leView on Github →