English
For α a seminormed additive commutative group, the space M_{m×n}(α) carries a SeminormedAddCommGroup structure with the norm defined as the sup over i of the L1-norms of the rows.
Русский
Для α — семинормированная аддитивная коммутативная группа пространство M_{m×n}(α) наделяется структурой SeminormedAddCommGroup с нормой, заданной как sup по строкам суммы норм элементов строки (L1-норма строки).
LaTeX
$$$\\|A\\|_{\\text{row}} = \\sup_{i \\in m} \\sum_{j \\in n} \\|A_{ij}\\|$$$
Lean4
/-- Seminormed group instance (using sup norm of L1 norm) for matrices over a seminormed group. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix. -/
@[local instance]
protected def linftyOpSeminormedAddCommGroup [SeminormedAddCommGroup α] : SeminormedAddCommGroup (Matrix m n α) :=
(by infer_instance : SeminormedAddCommGroup (m → PiLp 1 fun j : n => α))
