instMulAction — Mathlib

English

The scalar actions commute with internal addition, i.e., smul on LinearPMap respects addition.

Русский

Скалярные действия совместимы с операцией сложения внутри LinearPMap: a · (f + g) = a · f + a · g.

LaTeX

$$$a \cdot (f + g) = (a \cdot f) + (a \cdot g)$$$

Lean4

instance instMulAction : MulAction M (E →ₗ.[R] F)
    where
  smul := (· • ·)
  one_smul := fun ⟨_s, f⟩ => ext' <| one_smul M f
  mul_smul a b f := ext' <| mul_smul a b f.toFun

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