instContinuousSMul — Mathlib

English

For any R with a scalar action on A and a compatible topology, the scalar action on CStarMatrix(m,n,A) is continuous.

Русский

Для любого R со скалярным действием на A, совместимым топологическим устройством, скалярное умножение на CStarMatrix(m,n,A) непрерывно.

LaTeX

$$$$\\text{ContinuousSMul}(R,\\mathrm{CStarMatrix}(m,n,A)).$$$$

Lean4

instance instContinuousSMul {R : Type*} [SMul R A] [TopologicalSpace R] [ContinuousSMul R A] :
    ContinuousSMul R (CStarMatrix m n A) :=
  instContinuousSMulForall

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