instDistribMulActionOfSMulCommClassOfContinuousConstSMul

English

The additive structure on maps is built from the pointwise addition, with the zero map as the identity.

Русский

Аддитивная структура построена по точкам, нулевое отображение служит нейтральным элементом.

LaTeX

$$$ (f+g)^{\sim} = f^{\sim} + g^{\sim}, \ 0^{\sim} = 0$$$

Lean4

instance [Monoid S] [DistribMulAction S W] [SMulCommClass R S W] [ContinuousConstSMul S W] :
    DistribMulAction S (P →ᴬ[R] W) :=
  Function.Injective.distribMulAction ⟨⟨fun f ↦ f.toAffineMap.toFun, rfl⟩, coe_add⟩ coe_injective coe_smul

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