instSMulCommClass_1 — Mathlib

English

If 𝕜 acts boundedly on β, then the action commutes with the action on α →ᵇ β; i.e., smul on the function space commutes with pointwise operations.

Русский

Если 𝕜 действует на β ограниченно, тогда действие скаляра и действие на пространство функций коммутируют, т.е. скалярное умножение и точечные операции совместимы.

LaTeX

$$$\\text{If } SMulCommClass 𝕜 β β, \\ SMulCommClass 𝕜 (α \\to^b β) (\\alpha \\to^b β)$$$

Lean4

instance [SMulCommClass 𝕜 β β] : SMulCommClass 𝕜 (α →ᵇ β) (α →ᵇ β) where
  smul_comm _ _ _ := ext fun _ ↦ (mul_smul_comm ..).symm

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