modularForm — Mathlib

English

For fixed Γ and k, the collection ModularForm(Γ, k) carries a canonical ModularFormClass structure, encoding the slash-action, holomorphy, and cusp-boundedness properties.

Русский

Для фиксированных Γ и k множество ModularForm(Γ,k) обладает канонической структурой ModularFormClass, которая фиксирует действие слеша, голоморфность и ограниченность на бесконечностях.

LaTeX

$$$\mathrm{ModularFormClass}(\mathrm{ModularForm}(\Gamma,k),\Gamma,k)$$$

Lean4

instance (priority := 100) modularForm : ModularFormClass (ModularForm Γ k) Γ k
    where
  slash_action_eq f := f.slash_action_eq'
  holo := ModularForm.holo'
  bdd_at_cusps := ModularForm.bdd_at_cusps'

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