instIsScalarTower — Mathlib

English

There is a scalar tower structure for 𝕜', 𝕜 and (α →ᵇ β), compatible with smul and coe.

Русский

Существует структура стека скаляров для 𝕜', 𝕜 и (α →ᵇ β), совместимая с умножением и коэрцией.

LaTeX

$$$\text{IsScalarTower}(𝕜', 𝕜, (\alpha \to^{\mathrm{b}} β))$$$

Lean4

instance instIsScalarTower {𝕜' : Type*} [PseudoMetricSpace 𝕜'] [Zero 𝕜'] [SMul 𝕜' β] [IsBoundedSMul 𝕜' β] [SMul 𝕜' 𝕜]
    [IsScalarTower 𝕜' 𝕜 β] : IsScalarTower 𝕜' 𝕜 (α →ᵇ β) where smul_assoc _ _ _ := ext fun _ ↦ smul_assoc ..

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