instSMulCommClass' — Mathlib

English

For any appropriate scalar context M acting on R, the action of M commutes with the pointwise multiplication on C(X, R)₀; i.e., SMulCommClass M C(X, R)₀ C(X, R)₀ holds.

Русский

Пусть M — множество скаляров, действующее на R, тогда действие M на C(X, R)₀ commuting с операцией умножения по точкам; то есть SMulCommClass M C(X, R)₀ C(X, R)₀ выполняется.

LaTeX

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

Lean4

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

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