English
Let α be a normed algebra over a normed field R. Then the matrix algebra M_n(α) is a NormedAlgebra over R with the linfty operator norm defined as in the previous item.
Русский
Пусть α — нормированная алгебра над нормированной полем R. Тогда алгебра матриц M_n(α) является NormedAlgebra над R с линфити-операторной нормой, определённой как выше.
LaTeX
$$$M_n(\alpha)$ является NormedAlgebra over $R$ with $$\|A\| = \sup_{i} \sum_{j} \|a_{ij}\|.$$$$
Lean4
/-- Normed algebra instance (using sup norm of L1 norm) for matrices over a normed algebra. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix. -/
@[local instance]
protected def linftyOpNormedAlgebra [NormedField R] [SeminormedRing α] [NormedAlgebra R α] [DecidableEq n] :
NormedAlgebra R (Matrix n n α) :=
{ Matrix.linftyOpNormedSpace, Matrix.instAlgebra with }
