instSMulCommClass_2 — Mathlib

English

The standard monoid action of R on M induces a MulAction on C(α, M) by pointwise scalar multiplication.

Русский

Стандартное моноидальное действие R на M индуцирует MulAction на C(α, M) по точечному умножению на скаляры.

LaTeX

$$$ MulAction R C(\alpha, M). $$$

Lean4

instance [SMul R M] [ContinuousConstSMul R M] [Mul M] [ContinuousMul M] [SMulCommClass M R M] :
    SMulCommClass C(α, M) R C(α, M) where smul_comm _ _ _ := ext fun _ => smul_comm (_ : M) ..

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