isCentralScalar — Mathlib

English

If R is central relative to M, then R is central for Finsupp α M: the action by R on Finsupp commutes with the action on the function values.

Русский

Если R централизован по отношению к M, то R централен и для Finsupp α M: действие R на Finsupp коммутирует с действием на значения функции.

LaTeX

$$$IsCentralScalar R (\\alpha \\to_0 M)$$$

Lean4

instance isCentralScalar [Zero M] [SMulZeroClass R M] [SMulZeroClass Rᵐᵒᵖ M] [IsCentralScalar R M] :
    IsCentralScalar R (α →₀ M) where op_smul_eq_smul _ _ := ext fun _ => op_smul_eq_smul _ _

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