instSMulCommClassDomMulAct — Mathlib

English

Two DomMulAct actions define a commuting structure on the space of linear maps: SMulCommClass on LinearMap σ M M'.

Русский

Два действия DomMulAct задают структуру, в которой действие скаляров на отображениях коммутирует.

LaTeX

$$SMulCommClass (DomMulAct S') (DomMulAct T') (LinearMap σ M M')$$

Lean4

instance [SMulCommClass S' T' M] : SMulCommClass S'ᵈᵐᵃ T'ᵈᵐᵃ (M →ₛₗ[σ₁₂] M') :=
  ⟨fun s t f ↦ ext fun m ↦ by simp_rw [DomMulAct.smul_linearMap_apply, smul_comm]⟩

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