instSMulCommClass — Mathlib

English

There is a SMulCommClass structure on ContinuousMapZero X R ensuring scalar actions commute between different scalar sets M and N.

Русский

Существует структура SMulCommClass на ContinuousMapZero X R, обеспечивающая взаимную совместимость действий скалярами из M и N.

LaTeX

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

Lean4

instance instSMulCommClass {M N : Type*} [SMulZeroClass M R] [ContinuousConstSMul M R] [SMulZeroClass N R]
    [ContinuousConstSMul N R] [SMulCommClass M N R] : SMulCommClass M N C(X, R)₀ where
  smul_comm _ _ _ := ext fun _ ↦ smul_comm ..

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