instSMulCommClass' — Mathlib

English

There is a SMulCommClass instance ensuring that the scalar action of ℚ≥0 commutes with the action on S, i.e., q smul (a • b) = a • (q smul b) in the appropriate setting.

Русский

Существует экземпляр SMulCommClass, гарантирующий, что действие скаляра ℚ≥0 коммутирует с действием на S, то есть q smul (a • b) = a • (q smul b) в соответствующих условиях.

LaTeX

$$$$ \\text{SMulCommClass } \\mathbb{Q}_{\\ge 0} R S $$$$

Lean4

instance instSMulCommClass' [SMulCommClass S R S] : SMulCommClass R ℚ≥0 S :=
  have := SMulCommClass.symm S R S;
  SMulCommClass.symm _ _ _

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