instIsScalarTower — Mathlib

English

IsScalarTower holds for CStarMatrix: R, S act on A with a scalar tower structure, inducing IsScalarTower R S (CStarMatrix m n A).

Русский

Для CStarMatrix выполняется структура IsScalarTower R S (CStarMatrix m n A).

LaTeX

$$$[SMul R S] [SMul R A] [SMul S A] [IsScalarTower R S A], IsScalarTower R S (CStarMatrix m n A)$$$

Lean4

instance instIsScalarTower [SMul R S] [SMul R A] [SMul S A] [IsScalarTower R S A] :
    IsScalarTower R S (CStarMatrix m n A) :=
  Pi.isScalarTower

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