English
If α is a seminormed additive commutative group, the matrix space M_{m×n}(α) is equipped with a bounded scalar action, i.e., an IsBoundedSMul instance
Русский
Пусть α — семинормированная аддитивная коммутативная группа; пространство M_{m×n}(α) имеет ограниченное скалярное действие, то есть имеется экземпляр IsBoundedSMul
LaTeX
$$$\\text{IsBoundedSMul } R (\\mathrm{Mat}_{m\\times n}(\\alpha))$$$
Lean4
/-- This applies to the sup norm of L1 norm. -/
@[local instance]
protected theorem linftyOpIsBoundedSMul [SeminormedRing R] [SeminormedAddCommGroup α] [Module R α] [IsBoundedSMul R α] :
IsBoundedSMul R (Matrix m n α) :=
(by infer_instance : IsBoundedSMul R (m → PiLp 1 fun j : n => α))
