instIsScalarTowerSubtypeMem — Mathlib

English

If R', R, A are as above and S is a nonunital subalgebra of A, then the IsScalarTower property holds also for the subtype of units in S, i.e., IsScalarTower R (Subtype x∈S) (Subtype x∈S).

Русский

Если выполняются условия для R', R, A и S — ненулевая подпалгебра A, то свойство IsScalarTower сохраняется на подтипе элементов S.

LaTeX

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

Lean4

instance [IsScalarTower R A A] : IsScalarTower R S S where
  smul_assoc r x y := Subtype.ext <| smul_assoc r (x : A) (y : A)

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