instModule — Mathlib

English

If β is an R-module and the scalar action is continuous, then C₀(α,β) is an R-module with pointwise action.

Русский

Если β — модуль над R и скалярное действие непрерывно, то C₀(α,β) является модулем над R с покоординатным действием.

LaTeX

$$Module R C₀(α, β) under ContinuousConstSMul and standard pointwise operations.$$

Lean4

instance instModule [AddCommMonoid β] [ContinuousAdd β] {R : Type*} [Semiring R] [Module R β]
    [ContinuousConstSMul R β] : Module R C₀(α, β) :=
  Function.Injective.module R ⟨⟨_, coe_zero⟩, coe_add⟩ DFunLike.coe_injective coe_smul

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