instIsScalarTower — Mathlib

English

There is an IsScalarTower structure on ContinuousMapZero X R, relating nested scalar actions across M, N, and R.

Русский

Существует структура IsScalarTower для ContinuousMapZero X R, связывающая вложенные скалярные действия между M, N и R.

LaTeX

$$IsScalarTower M N (C(X,R)₀)$$

Lean4

instance instIsScalarTower {M N : Type*} [SMulZeroClass M R] [ContinuousConstSMul M R] [SMulZeroClass N R]
    [ContinuousConstSMul N R] [SMul M N] [IsScalarTower M N R] : IsScalarTower M N C(X, R)₀ where
  smul_assoc _ _ _ := ext fun _ ↦ smul_assoc ..

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