Theorem OnePoint.isBoundedAt_iff_exists_SL2Z

Modification history

2025-09-16 15:34
Mathlib/NumberTheory/ModularForms/BoundedAtCusp.lean
feat(NumberTheory/ModularForms): define boundedness / vanishing at a cusp (#29560)
Added OnePoint.isBoundedAt_iff_exists_SL2ZView on Github →