Theorems · Theorem · number theory

ModularFormClass.analyticAt_cuspFunction_zero

∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F)
  [ModularFormClass F Γ k], 0 < h → h ∈ Γ.strictPeriods → AnalyticAt ℂ (UpperHalfPlane.cuspFunction h ⇑f) 0

Defined in

Mathlib.NumberTheory.ModularForms.QExpansion

Cited by

14 results in Mathlib

Foundations

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

Assumes

FunLikeModularFormClass