Theorems · Theorem · number theory

ModularForm.qExpansion_mul_coe

∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2}
  [inst_1 : FunLike G UpperHalfPlane ℂ],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b],
        UpperHalfPlane.qExpansion h (⇑f * ⇑g) = UpperHalfPlane.qExpansion h ⇑f * UpperHalfPlane.qExpansion h ⇑g

The q-expansion of a pointwise product of two modular-form-class objects is the product of their q-expansions. Works for any ModularFormClass (e.g. a CuspForm times a ModularForm).

Defined in

Mathlib.NumberTheory.ModularForms.QExpansion

Cited by

2 results in Mathlib

Foundations

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

Assumes

FunLikeFunLikeModularFormClassModularFormClass