English
Let R be a normed field and α a normed space. Then the space M_{m×n}(α) is a NormedSpace over R, with the norm given by the sup-norm of the L1-row norm, i.e., ∥A∥ = sup_{i} ∑_{j} ∥A_{ij}∥.
Русский
Пусть R — нормированное поле, α — нормированное пространство. Тогда пространство M_{m×n}(α) является NormedSpace над R, норму которого задаёт супр-ну-строку L1 по строкам: ∥A∥ = sup_{i} ∑_{j} ∥A_{ij}∥.
LaTeX
$$$\\|A\\| = \\sup_{i \\in m} \\sum_{j \\in n} \\|A_{ij}\\|$$$
Lean4
/-- Normed space instance (using sup norm of sup 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. -/
protected def normedSpace : NormedSpace R (Matrix m n α) :=
Pi.normedSpace
