Theorems · Inductive type · number theory
CuspForm
Subgroup (GL (Fin 2) ℝ) → ℤ → Type
These are SlashInvariantForms that are holomorphic and zero at infinity.
- Defined in
- Mathlib.NumberTheory.ModularForms.Basic
- Cited by
- 36 results in Mathlib
- Foundations
- Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Matrixstatement · cited by 4,303
- Subgroupstatement · cited by 3,593
- Matrix.GeneralLinearGroupstatement · cited by 556
Cited by56
Results whose statement or proof uses this declaration.
- CuspForm.discriminantEquivstatement and proof · cited by 8
- CuspForm.discriminantstatement · cited by 7
- CuspForm.toModularFormₗstatement · cited by 7
- CuspForm.toSlashInvariantFormstatement and proof · cited by 4
- ModularForm.toCuspFormstatement · cited by 4
- CuspForm.translatestatement · cited by 3
- ModularForm.rank_eq_one_add_rank_cuspFormstatement · cited by 3
- CuspForm.rank_eq_zero_of_weight_lt_twelvestatement · cited by 2
- ModularForm.isCuspForm_iff_coeffZero_eq_zeroproof · cited by 2
- CuspForm.coe_discriminantstatement · cited by 1
- ModularForm.discriminant_mul_discriminantEquivstatement and proof · cited by 1
- CuspForm.discriminantEquiv_applystatement and proof · cited by 1