instModuleOfContinuousConstSMul — Mathlib

English

If β is a Module over a Semiring R with ContinuousConstSMul, then C_c(α,β) is a Module over R with pointwise scalar action.

Русский

Если β модуль над полем или полукольцом R и ContinuousConstSMul, то C_c(α,β) является модулем над R с точечным скалярным действием.

LaTeX

$$$$ \text{Module } R\ C_c(\alpha,\beta) $$$$

Lean4

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

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