English
Let R be a seminormed ring and α a seminormed additive commutative group with an R-module structure such that NormSMulClass R α holds. Then the matrix space M_{m×n}(α) carries NormSMulClass R, i.e., the scalar action is norm-bounded in the appropriate sense.
Русский
Пусть R — семинормированное кольцо, α — семинормированная аддитивная коммутативная группа с R-модулярной структурой и выполняется условие NormSMulClass R α. Тогда пространство матриц M_{m×n}(α) является NormSMulClass R: скалярное умножение нормально ограничено по норме.
LaTeX
$$$\\text{NormSMulClass } R (\\mathrm{Mat}_{m\\times n}(\\alpha))$$$
Lean4
/-- This applies to the sup norm of sup norm. -/
protected theorem normSMulClass [SeminormedRing R] [SeminormedAddCommGroup α] [Module R α] [NormSMulClass R α] :
NormSMulClass R (Matrix m n α) :=
Pi.instNormSMulClass
