instModularFormClassOfCuspFormClass

English

If a type F carries a FunLike structure on the upper half-plane and is equipped with a cusp form class property, then F Γ k forms a ModularFormClass; cusp forms generate modular form classes.

Русский

Если тип F имеет структуру FunLike на верхней полуплоскости и обладает свойством cusp form class, то F Γ k образует ModularFormClass; cusp формы образуют классы модулярных форм.

LaTeX

$$$\text{[FunLike } F \mathbb{H} \mathbb{C}]\;[\text{CuspFormClass } F \Gamma k]\;\Rightarrow\; \text{ModularFormClass } F \Gamma k.$$$

Lean4

instance (priority := 99) [FunLike F ℍ ℂ] [CuspFormClass F Γ k] : ModularFormClass F Γ k
    where
  slash_action_eq := SlashInvariantFormClass.slash_action_eq
  holo := CuspFormClass.holo
  bdd_at_cusps f _ hc g hg := (CuspFormClass.zero_at_cusps f hc g hg).boundedAtFilter

Похожие утверждения