instModuleReal — Mathlib

English

The collection of modular forms Γ k carries a natural real vector space structure, i.e., r · f is again a modular form and (r1 + r2) f = r1 f + r2 f.

Русский

Собрание модульных форм Γ k имеет естественную структуру вещественного векторного пространства: r · f снова модульная форма и (r1 + r2)f = r1 f + r2 f.

LaTeX

$$$ (r \cdot f)(z) = r \cdot f(z) \quad \text{for all } z, \ r \in \mathbb{R}. $$$

Lean4

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

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