instSMulCommClass — Mathlib

English

If α is locally compact and β is a ring with IsTopologicalRing, then C(α, β) is a topological ring under pointwise operations.

Русский

Если α локально компактно, а β — кольцо с IsTopologicalRing, то C(α, β) — топологическое кольцо по точечным операциям.

LaTeX

$$$ IsTopologicalRing\\ C(\\alpha, \\beta). $$$

Lean4

@[to_additive]
instance [SMul R M] [ContinuousConstSMul R M] [SMul R₁ M] [ContinuousConstSMul R₁ M] [SMulCommClass R R₁ M] :
    SMulCommClass R R₁ C(α, M) where smul_comm _ _ _ := ext fun _ => smul_comm _ _ _

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