English
For α a normed non-unital ring, Matrix n n α carries a NonUnitalNormedRing structure, extending the Linfty nonunital seminormed ring with the appropriate equality of norm and distance.
Русский
Для α — нормированного безединичного кольца, Matrix n×n α образует структуру NonUnitalNormedRing, расширяющую Linfty безединичную семинормированную структуру на соответствие норме и расстоянию.
LaTeX
$$$\\text{Matrix}_{n\\times n}(\\alpha)$ is a NonUnitalNormedRing with Linfty-type norm.$$
Lean4
/-- Normed non-unital ring instance (using sup norm of L1 norm) for matrices over a normed
non-unital ring. Not declared as an instance because there are several natural choices for defining
the norm of a matrix. -/
@[local instance]
protected def linftyOpNonUnitalNormedRing [NonUnitalNormedRing α] : NonUnitalNormedRing (Matrix n n α) :=
{ Matrix.linftyOpNonUnitalSemiNormedRing with eq_of_dist_eq_zero := eq_of_dist_eq_zero }
