instContinuousConstSMulMatrix — Mathlib

English

If α acts on R with a continuous constant scalar multiplication, then α acts on the matrix space entrywise.

Русский

Если α действует на R непрерывно константным умножением на скаляры, то α действует на пространстве матриц покомпонентно.

LaTeX

$$$\text{ContinuousConstSMul}(\alpha, M_{m,n}(R))$$$

Lean4

instance [SMul α R] [ContinuousConstSMul α R] : ContinuousConstSMul α (Matrix m n R) :=
  inferInstanceAs (ContinuousConstSMul α (m → n → R))

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