to_smulCommClass — Mathlib

English

In an R-algebra A, the actions of R on A and of A on itself commute: SMulCommClass R A A.

Русский

В алгебре A над R скаляры из R действуют на A и на A как на модуль самой A, причем эти действия commute: r • (a • x) = a • (r • x) для всех r∈R, a,x∈A.

LaTeX

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

Lean4

instance (priority := 200) to_smulCommClass {R A} [CommSemiring R] [Semiring A] [Algebra R A] : SMulCommClass R A A :=
  IsScalarTower.to_smulCommClass

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