apply_smulCommClass' — Mathlib

English

Under the same data as above, the commuting property holds with the sides reversed: the S-action commutes with the action by AlgEquiv on A1 in the symmetric sense.

Русский

При тех же данных верна симметричная версия свойства коммутирования между действием скаляров и действием через AlgEquiv на A1.

LaTeX

$$$\\forall s\\in S,\\; \\forall e \\in A_1 \\cong_{R} A_1,\\; \\forall a \\in A_1:\\ s\\cdot (e(a))=e(s\\cdot a).$$$

Lean4

instance apply_smulCommClass' {S} [SMul S R] [SMul S A₁] [IsScalarTower S R A₁] : SMulCommClass (A₁ ≃ₐ[R] A₁) S A₁ :=
  SMulCommClass.symm _ _ _

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