isCentralScalar — Mathlib

English

If S acts centrally on M, then S also acts centrally on the quotient M/N, making M/N a central S-module.

Русский

Если S действует как центральный скаляр на M, то аналогично S действует как центральный скаляр на M/N, делая его центральным S-модулем.

LaTeX

$$IsCentralScalar $S$ on $M/N$.$$

Lean4

instance isCentralScalar {S : Type*} [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] [SMul Sᵐᵒᵖ R]
    [Module Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] : IsCentralScalar S (M ⧸ N) :=
  Submodule.Quotient.isCentralScalar _

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