English
If α is a seminormed additive commutative group, then the set of m×n matrices with entries in α, endowed with the coordinatewise seminorm (sup norm over all entries), forms a SeminormedAddCommGroup. This norm is defined by ∥A∥ := sup_{i∈m} sup_{j∈n} ∥A_{ij}∥.
Русский
Если α — семинормированная аддитивная коммутативная группа, то множество матриц размера m×n со значениями в α, снабжённое покоординатной нормой (суп-нормой по всем элементам), образует Семиноморную аддитивную группу; норма задаётся как ∥A∥ = sup_i sup_j ∥A_{ij}∥.
LaTeX
$$$\text{Если } α\text{ — семиномерная аддитивная коммутативная группа, то } M_{m,n}(α)\text{ оснащено структурой } \text{SeminormedAddCommGroup} \text{ с нормой } ∥A∥ := \sup_{i}\sup_{j} ∥A_{ij}∥.$$$
Lean4
/-- Seminormed group instance (using sup norm of sup 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. -/
protected def seminormedAddCommGroup : SeminormedAddCommGroup (Matrix m n α) :=
Pi.seminormedAddCommGroup
