instGOneIntOfHasDetPlusMinusOneFinOfNatNatReal

English

If Γ has det ±1, the graded monoid of modular forms carries a distinguished unit element, with one defined as 1, acting as identity for multiplication.

Русский

Если детерминант Γ равен ±1, у градуированного моноида модульных форм есть выделенный единичный элемент, где one = 1, который служит единицей умножения.

LaTeX

$$$\text{instGOneIntOfHasDetPlusMinusOneFinOfNatNatReal}: \mathrm{GradedMonoid.GOne}(\mathrm{ModularForm}(\Gamma))$ с one = 1.$$

Lean4

instance (Γ : Subgroup (GL (Fin 2) ℝ)) [Γ.HasDetPlusMinusOne] : GradedMonoid.GOne (ModularForm Γ) where one := 1

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