English
Let R be a seminormed ring and α a seminormed additive commutative group with Module R α and NormSMulClass R α. Then Matrix m×n α has NormSMulClass R.
Русский
Пусть 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 L1 norm. -/
@[local instance]
protected theorem linftyOpNormSMulClass [SeminormedRing R] [SeminormedAddCommGroup α] [Module R α] [NormSMulClass R α] :
NormSMulClass R (Matrix m n α) :=
(by infer_instance : NormSMulClass R (m → PiLp 1 fun j : n => α))
