smulCommClass — Mathlib

English

If R and S act on M with SMulZeroClass structures and commute, then their actions commute on Finsupp α M as well.

Русский

Если действия R и S на M коммьютируют, то их действия на Finsupp α M также коммьютируют.

LaTeX

$$$SMulCommClass R S (\\alpha \\to_0 M)$$$

Lean4

instance smulCommClass [Zero M] [SMulZeroClass R M] [SMulZeroClass S M] [SMulCommClass R S M] :
    SMulCommClass R S (α →₀ M) where smul_comm _ _ _ := ext fun _ => smul_comm _ _ _

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