Theorems · Theorem · number theory

ModularForm.qExpansion_eq_qExpansion_discriminant_mul

∀ {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)
  (hcusp : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f) = 0),
  UpperHalfPlane.qExpansion 1 ⇑f =
    UpperHalfPlane.qExpansion 1 ModularForm.discriminant *
      UpperHalfPlane.qExpansion 1 ⇑(CuspForm.discriminantEquiv (f.toCuspForm hcusp))

The q-expansion of a level-1 modular form whose zeroth coefficient vanishes factors as the q-expansion of Δ times the q-expansion of the corresponding form of weight k - 12 obtained via discriminantEquiv.

Defined in

Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Cited by

1 results in Mathlib

Foundations

Depth 335 from the axioms · uses propext, Classical.choice, Quot.sound