English
The matrix space M_m×n(α) is a NormedSpace over R with the Frobenius norm, when α is a normed space over R.
Русский
Пространство матриц M_{m×n}(α) является NormedSpace над R с нормой Фробениуса, если α — нормированное пространство над R.
LaTeX
$$$M_{m\times n}(\alpha)$ is a NormedSpace over $R$ with the Frobenius norm.$$
Lean4
/-- Normed space instance (using the Frobenius norm) for matrices over a normed space. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix. -/
@[local instance]
def frobeniusNormedSpace [NormedField R] [SeminormedAddCommGroup α] [NormedSpace R α] : NormedSpace R (Matrix m n α) :=
(by infer_instance : NormedSpace R (PiLp 2 fun i : m => PiLp 2 fun j : n => α))
