English
Let α be a normed ring and n a finite index set. Then the set of n-by-n matrices over α, equipped with the linfty operator norm (the supremum of the row L1-norms), forms a NormedRing. In particular, addition and multiplication are compatible with this norm and the space is normed accordingly.
Русский
Пусть α — нормированное кольцо, и n — конечный индекс. Множество матриц размера n×n над α, снабжённое линфити-операторной нормой (супрумма норм элементов по строкам), образует NormedRing. В частности, сумма и произведение матриц совместимы с этой нормой, образуя нормированное пространство.
LaTeX
$$$(M_n(\alpha), \|\cdot\|_{linfty})$ является нормированным кольцом, где для $A=(a_{ij})$ определено $$\|A\|_{linfty} = \sup_{i} \sum_{j} \|a_{ij}\|.$$
$$
Lean4
/-- Normed ring 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 linftyOpNormedRing [NormedRing α] [DecidableEq n] : NormedRing (Matrix n n α) :=
{ Matrix.linftyOpSemiNormedRing with eq_of_dist_eq_zero := eq_of_dist_eq_zero }
