English
Let α be a normed additive commutative group. Then the set of all m × n matrices with entries in α carries a natural structure of a NormedAddCommGroup, given by the sup-norm taken entrywise (equivalently the sup over i∈m of the sup over j∈n of ∥Aij∥).
Русский
Пусть α — нормированная аддитивная коммутативная группа. Тогда множество всех матриц размером m×n над α наделено естественной структурой нормированной аддитивной коммутативной группы, норму которой задаёт супремум по всем элементам: ∥A∥ = sup_{i∈m} sup_{j∈n} ∥A_{ij}∥.
LaTeX
$$$\\|A\\| = \\sup_{i\\in m} \\sup_{j\\in n} \\|A_{ij}\\|,$$$
Lean4
/-- Normed group instance (using sup norm of sup norm) for matrices over a normed group. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix. -/
protected def normedAddCommGroup [NormedAddCommGroup α] : NormedAddCommGroup (Matrix m n α) :=
Pi.normedAddCommGroup
