instIsCentralScalar — Mathlib

English

There is a SMulCommClass and related IsCentralScalar structure making the scalar action on LinearMap commute with other actions.

Русский

Существуют структуры SMulCommClass и IsCentralScalar, обеспечивающие совместную согласованность скалярных действий на LinearMap.

LaTeX

$$$IsCentralScalar S (\mathrm{LinearMap} σ_{12} M M_2)$$$

Lean4

instance [DistribMulAction Sᵐᵒᵖ M₂] [SMulCommClass R₂ Sᵐᵒᵖ M₂] [IsCentralScalar S M₂] :
    IsCentralScalar S (M →ₛₗ[σ₁₂] M₂) where op_smul_eq_smul _ _ := ext fun _ ↦ op_smul_eq_smul _ _

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