isCentralScalar — Mathlib

English

If S acts centrally on R and M, then S acts centrally on the symmetrized type tsze R M.

Русский

Если S действует центрально на R и M, то S действует центрально на симметризованный тип tsze R M.

LaTeX

$$IsCentralScalar S (tsze R M)$$

Lean4

instance isCentralScalar [SMul S R] [SMul S M] [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsCentralScalar S R] [IsCentralScalar S M] :
    IsCentralScalar S (tsze R M) :=
  Prod.isCentralScalar

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