instSMulCommClass — Mathlib

English

There is an instance SMulCommClass G G' (Basis ι R M) ensuring the commuting actions on bases when both G and G' act on M.

Русский

Существует экземпляр SMulCommClass G G' (Basis ι R M), обеспечивающий коммутирование действий на базисах при действии на M обеих групп.

LaTeX

$$[SMulCommClass G G' (Basis ι R M)]$$

Lean4

instance [SMulCommClass G G' M] : SMulCommClass G G' (Basis ι R M) where
  smul_comm _g _g' _b := DFunLike.ext _ _ fun _ => smul_comm _ _ _

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