isCentralScalar — Mathlib

English

If S acts centrally on M and the scalar-tower conditions hold, then the SubMulAction p also has the central Scalar structure; the action of S on p commutes with the R-action when viewed through M.

Русский

При условии, что S действует центрально на M и соблюдаются условия башни скаляров, SubMulAction p также наследует центральное скалярное действие; действие S на p коммютирует с действием R, когда рассматривается через M.

LaTeX

$$$ IsCentralScalar S p $$$

Lean4

@[to_additive]
instance isCentralScalar [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] :
    IsCentralScalar S p where op_smul_eq_smul r x := Subtype.ext <| op_smul_eq_smul r (x : M)

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