instModuleReal — Mathlib

English

For any Γ ⊆ GL2(ℝ) with det 1 and weight k ∈ ℤ, the cusp forms space CuspForm(Γ,k) carries a natural structure of a real vector space (i.e., a real module).

Русский

Для любого подгруппы Γ в GL2(ℝ) с детерминантом 1 и веса k ∈ ℤ пространство cusp-form CuspForm(Γ,k) естественным образом является вещественным векторным пространством.

LaTeX

$$$\text{CuspForm}(\Gamma,k) \text{ is a } \mathbb{R}\text{-module}. $$$

Lean4

instance : Module ℝ (CuspForm Γ k) :=
  Function.Injective.module ℝ coeHom DFunLike.coe_injective fun _ _ => rfl

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