instIsScalarTower — Mathlib

English

Under a compatible web of scalar actions, Unitization R A inherits an IsScalarTower from the ambient towers.

Русский

При совместимой системе скаляров Unitization R A наследует IsScalarTower от окружающих башен.

LaTeX

$$$[SMul T R] [SMul T A] [SMul S R] [SMul S A] [IsScalarTower T S R] [IsScalarTower T S A] \\\\Rightarrow IsScalarTower T S (Unitization R A).$$$

Lean4

instance instIsScalarTower [SMul T R] [SMul T A] [SMul S R] [SMul S A] [SMul T S] [IsScalarTower T S R]
    [IsScalarTower T S A] : IsScalarTower T S (Unitization R A) :=
  Prod.isScalarTower

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