Theorem UpperHalfPlane.tendsto_smul_atImInfty

Modification history

2025-09-16 15:34
Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean
feat(NumberTheory/ModularForms): define boundedness / vanishing at a cusp (#29560)
Added UpperHalfPlane.tendsto_smul_atImInftyView on Github →