smulCommClass — Mathlib

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

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