instIsCentralScalar — Mathlib

English

The scalar action coming from a central scalar commutes with all operations in Unitization.

Русский

Действие скаляра, исходящее от центрального скаляра, коммутирует со всеми операциями в Unitization.

LaTeX

$$$[SMul S R] [SMul S A] [SMul (MulOpposite S) R] [SMul (MulOpposite S) A] [IsCentralScalar S R] [IsCentralScalar S A] \\\\Rightarrow IsCentralScalar S (Unitization R A).$$$

Lean4

instance instIsCentralScalar [SMul S R] [SMul S A] [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ A] [IsCentralScalar S R]
    [IsCentralScalar S A] : IsCentralScalar S (Unitization R A) :=
  Prod.isCentralScalar

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