English
For α a seminormed ring, the family Matrix n n α carries a SeminormedRing structure via the Linfty norm; the usual ring operations are compatible with this norm.
Русский
Для α — семинормированного кольца, матричный набор Matrix n×n α наделяется семинормированным кольцом, используя норму Linfty; операции умножения и сложения совместимы с нормой.
LaTeX
$$$\\text{Matrix}_{n\\times n}(\\alpha)$ is a SeminormedRing under the Linfty norm.$$
Lean4
/-- Seminormed ring instance (using sup norm of L1 norm) for matrices over a semi normed ring. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix. -/
@[local instance]
protected def linftyOpSemiNormedRing [SeminormedRing α] [DecidableEq n] : SeminormedRing (Matrix n n α) :=
{ Matrix.linftyOpNonUnitalSemiNormedRing, Matrix.instRing with }
