instSMulCommClass — Mathlib

English

There is a base instance showing SMulCommClass S T (LieDerivation R L M) given SMulCommClass S M and SMulCommClass T M, ensuring the commuting of scalar actions across S and T.

Русский

Существует базовый инстанс SMulCommClass S T (LieDerivation R L M), если заданы SMulCommClass S M и SMulCommClass T M, что обеспечивает совместное действие скаляров S и T.

LaTeX

$$$\text{SMulCommClass } S T (\text{LieDerivation } R L M)$$$

Lean4

instance [SMulCommClass S T M] : SMulCommClass S T (LieDerivation R L M) :=
  ⟨fun _ _ _ => ext fun _ => smul_comm _ _ _⟩

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