English
For α a normed additive commutative group, the space M_{m×n}(α) inherits a NormedAddCommGroup structure via the Linfty path, i.e., the norm is the sup over i of the Linfty norm of the i-th row.
Русский
Для α — нормированная аддитивная коммутативная группа пространство M_{m×n}(α) наследует структуру NormedAddCommGroup через норму Linfty: ‖A‖ = sup_i ‖A_i‖_{∞}, где A_i — i-я строка.
LaTeX
$$$\\|A\\| = \\sup_{i\\in m} \\| (A_{i j})_{j\\in n} \\|_{\\infty}$$$
Lean4
/-- Normed group instance (using sup norm of L1 norm) for matrices over a normed ring. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix. -/
@[local instance]
protected def linftyOpNormedAddCommGroup [NormedAddCommGroup α] : NormedAddCommGroup (Matrix m n α) :=
(by infer_instance : NormedAddCommGroup (m → PiLp 1 fun j : n => α))
