instMulActionWithZero — Mathlib

English

There is a MulActionWithZero of R on C₀(α,β) given by pointwise action.

Русский

Существует действие множителя с нулём, задающееся по точкам.

LaTeX

$$MulActionWithZero R C₀(α, β) with (r • f)(x) = r • f(x).$$

Lean4

instance instMulActionWithZero [Zero β] {R : Type*} [MonoidWithZero R] [MulActionWithZero R β]
    [ContinuousConstSMul R β] : MulActionWithZero R C₀(α, β) :=
  Function.Injective.mulActionWithZero ⟨_, coe_zero⟩ DFunLike.coe_injective coe_smul

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