instIsScalarTowerUniformFun — Mathlib

English

If β is an M–N bimodule with IsScalarTower M N β, then the function-valued space α →ᵤ β inherits the same tower structure: IsScalarTower M N (α →ᵤ β).

Русский

Если β имеет структуру M–N-модуля с условием IsScalarTower M N β, то пространство функций α →ᵤ β также имеет такую же цепочку: IsScalarTower M N (α →ᵤ β).

LaTeX

$$$\text{IsScalarTower } M N \beta \rightarrow \text{IsScalarTower } M N (\alpha \to^\mathrm{u} \beta).$$$

Lean4

instance {M N : Type*} [SMul M N] [SMul M β] [SMul N β] [IsScalarTower M N β] : IsScalarTower M N (α →ᵤ β) :=
  Pi.isScalarTower

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