instDistribMulAction — Mathlib

English

The scalar action distributes over addition for bounded continuous functions: (a + b) • f = a • f + b • f and a • (f + g) = a • f + a • g.

Русский

Скалярное умножение распадается на сумму по отношению к сложению: (a + b) • f = a • f + b • f и a • (f + g) = a • f + a • g.

LaTeX

$$$DistribMulAction_{\\mathbb{K}}(\\alpha \\to^{\\mathrm{b}} \\beta)$$$

Lean4

instance instDistribMulAction : DistribMulAction 𝕜 (α →ᵇ β) :=
  DFunLike.coe_injective.distribMulAction ⟨⟨_, coe_zero⟩, coe_add⟩ coe_smul

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