instIsScalarTower' — Mathlib

English

There is a compatibility (IsScalarTower) between the scalars M, the ring C(X, R)₀, and itself, i.e., smul associativity holds when M acts via scalars on C(X, R)₀.

Русский

Существует совместимость (IsScalarTower) между скалярами M, кольцом C(X, R)₀ и самим собой: скалярное умножение ассоциативно через единицы.

LaTeX

$$$\text{IsScalarTower } M\ (C(X, R)₀)\ (C(X, R)₀)$$$

Lean4

instance instIsScalarTower' {M : Type*} [SMulZeroClass M R] [IsScalarTower M R R] [ContinuousConstSMul M R] :
    IsScalarTower M C(X, R)₀ C(X, R)₀ where smul_assoc m f g := ext fun x ↦ smul_assoc m (f x) (g x)

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