isScalarTower — Mathlib

English

If R,S α form a scalar tower and act compatibly on α, then Matrix m n α also forms IsScalarTower R S.

Русский

Если R,S α образуют скалярную башню и совместно действуют на α, то Matrix m n α также образует IsScalarTower.

LaTeX

$$$ [SMul\ R\ S] [SMul\ R\ α] [SMul\ S\ α] [IsScalarTower\ R\ S\ α] \Rightarrow IsScalarTower\ R\ S (Matrix\ m\ n\ α) $$$

Lean4

instance isScalarTower [SMul R S] [SMul R α] [SMul S α] [IsScalarTower R S α] : IsScalarTower R S (Matrix m n α) :=
  Pi.isScalarTower

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