Theorems · Theorem · number theory

ModularForm.cuspFunction_sub

∀ {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.cuspFunction h (⇑f - ⇑g) = UpperHalfPlane.cuspFunction h ⇑f - UpperHalfPlane.cuspFunction h ⇑g

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

FunLikeFunLikeModularFormClassModularFormClass