Theorems · Theorem · number theory

ModularForm.qExpansion_of_mul

∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [inst : Γ.HasDetPlusMinusOne],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ (a b : ℤ) (f : ModularForm Γ a) (g : ModularForm Γ b),
        UpperHalfPlane.qExpansion h
            ⇑(((DirectSum.of (ModularForm Γ) a) f * (DirectSum.of (ModularForm Γ) b) g) (a + b)) =
          UpperHalfPlane.qExpansion h ⇑f * UpperHalfPlane.qExpansion h ⇑g

Defined in

Mathlib.NumberTheory.ModularForms.QExpansion

Cited by

0 results in Mathlib

Foundations

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

Assumes

Subgroup.HasDetPlusMinusOne