instSMulWithZero — Mathlib

English

If β has a zero and SMulWithZero, then C₀(α,β) inherits SMulWithZero structure.

Русский

Если β имеет ноль и SMulWithZero, то C₀(α,β) наследует структуру SMulWithZero.

LaTeX

$$SMulWithZero R C₀(α, β) given [Zero β], [SMulWithZero R β], [ContinuousConstSMul R β].$$

Lean4

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

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