instGMulIntOfHasDetPlusMinusOneFinOfNatNatReal

English

If Γ is a subgroup with determinant ±1, the collection of modular forms on Γ is closed under multiplication and carries a natural graded multiplication, forming a graded monoid.

Русский

Если Γ — подгруппа с детерминантом ±1, множество модульных форм на Γ замыкается при умножении и имеет естественное градуированное умножение, образуя градуированную моноиду.

LaTeX

$$$\\{f,g\\} \\subseteq \\mathrm{ModularForm}(Γ) \\quad \\Rightarrow \\quad f \\cdot g \\in \\mathrm{ModularForm}(Γ),$ \\\\ and the product respects the grading: if $f\\in M_k(Γ)$ and $g\\in M_l(Γ)$ then $fg\\in M_{k+l}(Γ)$.$$

Lean4

instance (Γ : Subgroup (GL (Fin 2) ℝ)) [Γ.HasDetPlusMinusOne] : GradedMonoid.GMul (ModularForm Γ) where
  mul f g := f.mul g

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