Theorems · Definition · number theory

ModularForm.toCuspForm

{k : ℤ} →
  (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
    (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) = 0 → CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k

Build a CuspForm 𝒮ℒ k from a ModularForm 𝒮ℒ k whose q-expansion has vanishing constant term. The resulting cusp form has the same underlying function.

Defined in: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
Cited by: 4 results in Mathlib
Foundations: Depth 295 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Realstatement and proof · cited by 25,697
RingHom.idstatement · cited by 18,349
LinearMapstatement · cited by 10,215
Complexstatement · cited by 5,565
Matrixstatement · cited by 4,303
PowerSeriesstatement · cited by 797
UpperHalfPlanestatement · cited by 626
Matrix.GeneralLinearGroupstatement · cited by 556
Matrix.SpecialLinearGroupstatement · cited by 348
PowerSeries.coeffstatement and proof · cited by 324
MonoidHom.rangestatement and proof · cited by 314

Cited by4

Results whose statement or proof uses this declaration.

ModularForm.qExpansion_eq_qExpansion_discriminant_mulstatement and proof · cited by 1
ModularForm.sturm_bound_levelOne_natproof · cited by 1
ModularForm.toCuspForm_applystatement · cited by 0
ModularForm.toCuspForm.congr_simpstatement and proof · cited by 0