instMulActionWithZeroOfContinuousConstSMul

English

If β is Zero and MonoidWithZero with ContinuousConstSMul, then C_c(α,β) carries MulActionWithZero: multiplication with zero respects zero and distribution holds.

Русский

Если β имеет нуль и умножение с нулём, тогда C_c(α,β) имеет MulActionWithZero: умножение на ноль даёт ноль и распределение выполняется.

LaTeX

$$$$ (r\cdot f) = f \nobreak\text{(componentwise action)} $$$$

Lean4

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

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