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 }⟩