instModuleDomMulActOfSMulCommClass

English

There is a module structure over DomMulAct on the space of linear maps M → M', i.e., LinearMap σ M M' is a module over DomMulAct S.

Русский

Пространство линейных отображений имеет модульную структуру над DomMulAct; линейные отображения образуют модуль над DomMulAct S.

LaTeX

$$Module (DomMulAct S) (LinearMap σ M M')$$

Lean4

instance [SMulCommClass R S M] : Module Sᵈᵐᵃ (M →ₛₗ[σ₁₂] M')
    where
  add_smul _ _ _ := ext fun _ ↦ by simp_rw [add_apply, DomMulAct.smul_linearMap_apply, ← map_add, ← add_smul]; rfl
  zero_smul _ := ext fun _ ↦ by erw [DomMulAct.smul_linearMap_apply, zero_smul, map_zero]; rfl

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