instSMulCommClass — Mathlib

English

If SMulCommClass R A A holds, then SMulCommClass R' R S also holds, i.e., scalar actions commute on the subalgebra S.

Русский

Если выполняется SMulCommClass R A A, то выполняется SMulCommClass R' R S на подпалгебре S: действия скаляров коммутируют на S.

LaTeX

$$$ \\forall r' \\in R',\\ \\forall r \\in R,\\ \\forall s \\in S:\\ r' (r s) = r (r' s). $$$

Lean4

instance instSMulCommClass [SMulCommClass R A A] : SMulCommClass R S S where
  smul_comm r x y := Subtype.ext <| smul_comm r (x : A) (y : A)

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