English
The direct sum of modular forms over Γ carries a commutative ring structure, with componentwise addition and multiplication induced from modular form multiplication.
Русский
Прямой сумма модульных форм на Γ образует коммутативное кольцо, операции сложения и умножения определяются компонентно и наследуют умножение модульных форм.
LaTeX
$$$\\bigoplus_{k} M_k(Γ)$ is a commutative ring with addition and multiplication induced by those on ModularForm Γ.$$
Lean4
instance instGCommRing (Γ : Subgroup (GL (Fin 2) ℝ)) [Γ.HasDetPlusMinusOne] : DirectSum.GCommRing (ModularForm Γ)
where
one_mul _ := gradedMonoid_eq_of_cast (zero_add _) (ext fun _ => one_mul _)
mul_one _ := gradedMonoid_eq_of_cast (add_zero _) (ext fun _ => mul_one _)
mul_assoc _ _ _ := gradedMonoid_eq_of_cast (add_assoc _ _ _) (ext fun _ => mul_assoc _ _ _)
mul_zero {_ _} _ := ext fun _ => mul_zero _
zero_mul {_ _} _ := ext fun _ => zero_mul _
mul_add {_ _} _ _ _ := ext fun _ => mul_add _ _ _
add_mul {_ _} _ _ _ := ext fun _ => add_mul _ _ _
mul_comm _ _ := gradedMonoid_eq_of_cast (add_comm _ _) (ext fun _ => mul_comm _ _)
natCast := Nat.cast
natCast_zero := ext fun _ => Nat.cast_zero
natCast_succ _ := ext fun _ => Nat.cast_succ _
intCast := Int.cast
intCast_ofNat _ := ext fun _ => AddGroupWithOne.intCast_ofNat _
intCast_negSucc_ofNat _ := ext fun _ => AddGroupWithOne.intCast_negSucc _
