instIsScalarTower — Mathlib

English

If E is an R-module and an R'-module with a scalar tower IsScalarTower R R' E, then WithCStarModule A E inherits a canonical IsScalarTower R R' (WithCStarModule A E).

Русский

Если E является R-модулем и R'-модулем с тензорной (цепью) скаляров IsScalarTower R R' E, то WithCStarModule A E наследует стандартную цепь скаляров IsScalarTower R R' (WithCStarModule A E).

LaTeX

$$$ IsScalarTower R R' E \implies IsScalarTower R R' (WithCStarModule A E)$$

Lean4

instance instIsScalarTower [SMul R R'] [SMul R E] [SMul R' E] [IsScalarTower R R' E] : IsScalarTower R R' C⋆ᵐᵒᵈ(A, E) :=
  ‹IsScalarTower R R' E›

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