Structures · Algebra
CuspFormClass
CuspFormClass F Γ k says that F is a type of bundled functions that extend
SlashInvariantFormClass by requiring that the functions be holomorphic and zero
at all cusps.
- Defined in
- Mathlib.NumberTheory.ModularForms.Basic
- Shape
- 3 explicit arguments · adds holo, zero_at_cusps
Extends1
Extended by0
Nothing extends this class yet.
Forgetful instances
Every CuspFormClass is also a
Concrete types that are instances1
- CuspForm
How is a type an instance?
Loading the hierarchy index…
Assumed by25
- CuspFormClass.zero_at_infty
- CuspForm.translate
- CuspForm.isStrongFEPair
- CuspFormClass.petersson_bounded_left
- CuspFormClass.zero_at_cusps
- CuspFormClass.holo
- CuspForm.hasSum_Λ
- CuspForm.Λ_eq_mellin
- CuspForm.trace
- CuspForm.differentiable_Λ
- CuspFormClass.qExpansion_coeff_zero
- CuspFormClass.exp_decay_atImInfty
- CuspFormClass.cuspFunction_apply_zero
- CuspFormClass.exists_bound
- CuspFormClass.qExpansion_isBigO
- CuspFormClass.exp_decay_atImInfty'
- CuspForm.hasSum_L
- CuspFormClass.toSlashInvariantFormClass
- CuspFormClass.petersson_bounded_right
- CuspForm.differentiable_L
- CuspFormClass.zero_at_infty_slash
- CuspForm.coe_trace
- CuspForm.instModularFormClassOfCuspFormClass
- CuspForm.coe_translate
- CuspFormClass.zero_at_infty_comp_ofComplex