Theorems · Theorem · number theory

ModularFormClass.qExpansion_coeff_unique

∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {c : ℕ → ℂ},
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ {f : F} [ModularFormClass F Γ k],
        (∀ (τ : UpperHalfPlane), HasSum (fun m => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) →
          ∀ (m : ℕ), c m = (PowerSeries.coeff m) (UpperHalfPlane.qExpansion h ⇑f)

Defined in

Mathlib.NumberTheory.ModularForms.QExpansion

Cited by

1 results in Mathlib

Foundations

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

Assumes

FunLikeModularFormClass