English
The L₁–L∞ norm preserves one on nonempty matrices: the matrix space M_{n×n}(α) carries NormOneClass with norm of the identity equal to 1.
Русский
Нормированная единичная матричная структура сохраняется: пространство матриц M_{n×n}(α) имеет NormOneClass и норма единичного матрица равна 1.
LaTeX
$$$\\text{NormOneClass } (\\mathrm{Mat}_{n\\times n}(\\alpha))$, with the norm of the identity matrix equal to 1.$$
Lean4
/-- The `L₁-L∞` norm preserves one on non-empty matrices. Note this is safe as an instance, as it
carries no data. -/
instance linfty_opNormOneClass [SeminormedRing α] [NormOneClass α] [DecidableEq n] [Nonempty n] :
NormOneClass (Matrix n n α) where norm_one := (linfty_opNorm_diagonal _).trans norm_one
