to_smulCommClass' — Mathlib

English

Let R,A,M be as above. The swapped commutation instance holds: the actions of A and R on M commute in the opposite order, i.e., SMulCommClass A R M.

Русский

Пусть R,A,M удовлетворяют условиям. Переопределённый класс SMulCommClass между A и R на M означает, что их действия взаимно commute: a • (r • m) = r • (a • m) для всех a∈A, r∈R, m∈M.

LaTeX

$$$\\forall a\\in A\\, \\forall r\\in R\\, \\forall m\\in M:\\ a \\cdot (r \\cdot m) = r \\cdot (a \\cdot m)$$$

Lean4

instance (priority := 110) to_smulCommClass' : SMulCommClass A R M :=
  SMulCommClass.symm _ _
    _
      -- see Note [lower instance priority]

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