smulCommClass — Mathlib

English

There is a SMulCommClass structure for N and O acting on MonoidAlgebra R M when N and O act compatibly on R and commute with each other.

Русский

Существует структура SMulCommClass для N и O, действующих на MonoidAlgebra R M, когда действия согласованы на R и коммутируют между собой.

LaTeX

$$$\\text{SMulCommClass } N\\ O\\ (MonoidAlgebra\\ R\\ M)$$$

Lean4

@[to_additive (dont_translate := N) smulCommClass]
instance smulCommClass [SMulZeroClass N R] [SMulZeroClass O R] [SMulCommClass N O R] :
    SMulCommClass N O (MonoidAlgebra R M) :=
  Finsupp.smulCommClass ..

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