Commit 2024-01-09 14:39 9d2a0f8b

feat: provide the ℓ² operator norm on matrices (#9474) This adds the (unique) C⋆-norm on matrices Matrix n n 𝕜 with IsROrC 𝕜 within the scope Matrix.L2OpNorm. This norm coincides with the operator norm induced by the ℓ² norm (i.e., the norm on Matrix m n 𝕜 obtained by pulling back the norm from EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 m). Where possible, we state results for rectangular matrices.