instIsScalarTower' — Mathlib

English

Let R' be a semiring acting on R and on A, with A a module over R and IsScalarTower(R',R,A). If S is a nonunital subalgebra of A, then S inherits an IsScalarTower structure: for all r' in R', r in R, s in S, (r' r) • s = r' • (r • s).

Русский

Пусть R' — полугруппа, действующая на R и на A, A модуль над R и выполняется условие IsScalarTower(R',R,A). Тогда S, ненулевой подпалгебра A, наследует структуру IsScalarTower: для всех r' в R', r в R, s в S выполняется (r' r) • s = r' • (r • 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 instIsScalarTower' [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] : IsScalarTower R' R S :=
  S.toSubmodule.isScalarTower

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