instIsCentralScalar — Mathlib

English

CStarMatrix m n A has a central scalar structure: scalar actions by R commute with all endomorphisms on matrices; i.e., IsCentralScalar R (CStarMatrix m n A).

Русский

Для CStarMatrix m n A скаляры центральны по отношению к действию скаляров.

LaTeX

$$$[SMul R A] [SMul R^\text{op} A] [IsCentralScalar R A] : IsCentralScalar R (CStarMatrix m n A)$$$

Lean4

instance instIsCentralScalar [SMul R A] [SMul Rᵐᵒᵖ A] [IsCentralScalar R A] : IsCentralScalar R (CStarMatrix m n A) :=
  Pi.isCentralScalar

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