English
If α carries SMul by R and by S and these actions commute appropriately, then Matrix m n α has SMulCommClass R S.
Русский
Если у α есть действия SMul R и SMul S, которые взаимно приводимы к коммутатии, тогда Matrix m n α обладает SMulCommClass R S.
LaTeX
$$$ [SMul\ R\ α] [SMul\ S\ α] [SMulCommClass\ R\ S\ α] \Rightarrow SMulCommClass\ R\ S (Matrix\ m\ n\ α) $$$
Lean4
instance smulCommClass [SMul R α] [SMul S α] [SMulCommClass R S α] : SMulCommClass R S (Matrix m n α) :=
Pi.smulCommClass