instGAlgebra — Mathlib

English

The direct sum of modular forms on Γ is endowed with a ℂ-algebra structure.

Русский

Прямая сумма модульных форм на Γ снабжена структурой алгебры над комплексными числами.

LaTeX

$$$\\bigoplus_{k} M_k(Γ) \\quad \\text{is a }\\ \\mathbb{C}\\text{-algebra}. $$$

Lean4

instance instGAlgebra (Γ : Subgroup (GL (Fin 2) ℝ)) [Γ.HasDetOne] : DirectSum.GAlgebra ℂ (ModularForm Γ)
    where
  toFun := { toFun z := const z, map_zero' := rfl, map_add' := fun _ _ => rfl }
  map_one := rfl
  map_mul _x _y := rfl
  commutes _c _x := gradedMonoid_eq_of_cast (add_comm _ _) (ext fun _ => mul_comm _ _)
  smul_def _x _x := gradedMonoid_eq_of_cast (zero_add _).symm (ext fun _ => rfl)

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