isScalarTower — Mathlib

English

The actions of R and S on End(A) form a scalar tower: applying r then s is the same as applying the composite rs to End(A).

Русский

Действия R и S на End(A) образуют тензорную(каскадную) структуру: (r • (s • f)) = (rs) • f.

LaTeX

$$$ [IsScalarTower\ R\ S\ (\mathrm{End}(A))] \\ \forall r\in R, s\in S, f\in \mathrm{End}(A): (r \cdot (s \cdot f)) = ((r s) \cdot f)$$$

Lean4

instance isScalarTower [SMul R S] [IsScalarTower R S A] : IsScalarTower R S (AddMonoid.End A) :=
  AddMonoidHom.instIsScalarTower

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