instSMul — Mathlib

English

There is a scalar action of M on LinearPMap given by (a • f) with the same domain and (a • f)(x) = a • f(x).

Русский

Существует скалярное действие множества M на LinearPMap: (a • f) имеет ту же область определения и (a • f)(x) = a • f(x).

LaTeX

$$$\forall a \in M,\ f \in (E \to_{R}^{\mathrm{LinearPMap}} F),\ (a \cdot f).\mathrm{domain} = f.\mathrm{domain} \ \land\ \forall x,\ (a \cdot f) x = a \cdot f x$$$

Lean4

instance instSMul : SMul M (E →ₗ.[R] F) :=
  ⟨fun a f =>
    { domain := f.domain
      toFun := a • f.toFun }⟩

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