instSMulCommClass_1 — Mathlib

English

The IsScalarTower instance for R, R1 acting on C(α, M) holds, i.e., associativity of smul across layers for continuous maps.

Русский

Существуют структуры IsScalarTower для R, R1 на C(α, M) и т.д., обеспечивающие ассоциативность умножения скаляров.

LaTeX

$$$ IsScalarTower R R1 (C(\alpha, M)). $$$

Lean4

instance [SMul R M] [ContinuousConstSMul R M] [Mul M] [ContinuousMul M] [SMulCommClass R M M] :
    SMulCommClass R C(α, M) C(α, M) where smul_comm _ _ _ := ext fun _ => (mul_smul_comm ..).symm

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