instIsScalarTower — Mathlib

English

There is a MulAction of M on LinearPMap, i.e., a compatible binary action satisfying the usual axioms.

Русский

Существует действие умножения M на LinearPMap, удовлетворяющее обычным аксиомам.

LaTeX

$$$MulAction\ M\ (E \to_{R}^{\mathrm{LinearPMap}} F)$$$

Lean4

instance instIsScalarTower [SMul M N] [IsScalarTower M N F] : IsScalarTower M N (E →ₗ.[R] F) :=
  ⟨fun a b f => ext' <| smul_assoc a b f.toFun⟩

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