apply_smulCommClass' — Mathlib

English

Symmetric version of smul commutativity: for all r, e, m, r • (e • m) = (r • e) • m.

Русский

Симметричная версия свойства: для всех r, e, m верно r • (e • m) = (r • e) • m.

LaTeX

$$$\\forall r\\in S, \\forall e\\in \\mathrm{End}_R(M), \\forall m\\in M,\\ r\\cdot (e\\cdot m) = (r\\cdot e)\\cdot m.$$$

Lean4

instance apply_smulCommClass' [SMul S R] [SMul S M] [IsScalarTower S R M] : SMulCommClass (Module.End R M) S M :=
  SMulCommClass.symm _ _ _

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