isCentralScalar — Mathlib

English

If α carries a scalar action that is central, then Matrix m n α has IsCentralScalar.

Русский

Если α имеет центральное скалярное действие, тогда Matrix m n α имеет IsCentralScalar.

LaTeX

$$$ [SMul\ R\ α] [SMul\ R\ᵐᵒᵖ α] [IsCentralScalar\ R\ α] \Rightarrow IsCentralScalar\ R (Matrix\ m\ n\ α) $$$

Lean4

instance isCentralScalar [SMul R α] [SMul Rᵐᵒᵖ α] [IsCentralScalar R α] : IsCentralScalar R (Matrix m n α) :=
  Pi.isCentralScalar

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