smulCommClass_left — Mathlib

English

The induced left action inherits the smul-commuting property: elements of S commute with the action on β when acting on α.

Русский

Унаследованное левое действие сохраняет свойство коммутирования умножения: элементы S коммутируют с действием на β, действуя на α.

LaTeX

$$$SMulCommClass(S, \alpha, \beta)$$$

Lean4

instance smulCommClass_left [SMul A β] [SMul α β] [SMulCommClass A α β] (S : Subalgebra R A) : SMulCommClass S α β :=
  S.toSubsemiring.smulCommClass_left

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