# Matrices as a normed space #

In this file we provide the following non-instances for norms on matrices:

• The elementwise norm:

• Matrix.seminormedAddCommGroup
• Matrix.normedAddCommGroup
• Matrix.normedSpace
• Matrix.boundedSMul
• The Frobenius norm:

• Matrix.frobeniusSeminormedAddCommGroup
• Matrix.frobeniusNormedAddCommGroup
• Matrix.frobeniusNormedSpace
• Matrix.frobeniusNormedRing
• Matrix.frobeniusNormedAlgebra
• Matrix.frobeniusBoundedSMul
• The $L^\infty$ operator norm:

• Matrix.linftyOpSeminormedAddCommGroup
• Matrix.linftyOpNormedAddCommGroup
• Matrix.linftyOpNormedSpace
• Matrix.linftyOpBoundedSMul
• Matrix.linftyOpNonUnitalSemiNormedRing
• Matrix.linftyOpSemiNormedRing
• Matrix.linftyOpNonUnitalNormedRing
• Matrix.linftyOpNormedRing
• Matrix.linftyOpNormedAlgebra

These are not declared as instances because there are several natural choices for defining the norm of a matrix.

The norm induced by the identification of Matrix m n 𝕜 with EuclideanSpace n 𝕜 →L[𝕜] EuclideanSpace m 𝕜 (i.e., the ℓ² operator norm) can be found in Analysis.NormedSpace.Star.Matrix. It is separated to avoid extraneous imports in this file.

### The elementwise supremum norm #

def Matrix.seminormedAddCommGroup {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] :

Seminormed group instance (using sup norm of sup norm) for matrices over a seminormed group. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations
Instances For
theorem Matrix.norm_def {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] (A : Matrix m n α) :
A = fun (i : m) (j : n) => A i j
theorem Matrix.norm_eq_sup_sup_nnnorm {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] (A : Matrix m n α) :
A = (Finset.univ.sup fun (i : m) => Finset.univ.sup fun (j : n) => A i j‖₊)

The norm of a matrix is the sup of the sup of the nnnorm of the entries

theorem Matrix.nnnorm_def {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] (A : Matrix m n α) :
A‖₊ = fun (i : m) (j : n) => A i j‖₊
theorem Matrix.norm_le_iff {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] {r : } (hr : 0 r) {A : Matrix m n α} :
A r ∀ (i : m) (j : n), A i j r
theorem Matrix.nnnorm_le_iff {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] {r : NNReal} {A : Matrix m n α} :
A‖₊ r ∀ (i : m) (j : n), A i j‖₊ r
theorem Matrix.norm_lt_iff {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] {r : } (hr : 0 < r) {A : Matrix m n α} :
A < r ∀ (i : m) (j : n), A i j < r
theorem Matrix.nnnorm_lt_iff {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] {r : NNReal} (hr : 0 < r) {A : Matrix m n α} :
A‖₊ < r ∀ (i : m) (j : n), A i j‖₊ < r
theorem Matrix.norm_entry_le_entrywise_sup_norm {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] (A : Matrix m n α) {i : m} {j : n} :
theorem Matrix.nnnorm_entry_le_entrywise_sup_nnnorm {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] (A : Matrix m n α) {i : m} {j : n} :
@[simp]
theorem Matrix.nnnorm_map_eq {m : Type u_3} {n : Type u_4} {α : Type u_5} {β : Type u_6} [] [] (A : Matrix m n α) (f : αβ) (hf : ∀ (a : α), f a‖₊ = a‖₊) :
@[simp]
theorem Matrix.norm_map_eq {m : Type u_3} {n : Type u_4} {α : Type u_5} {β : Type u_6} [] [] (A : Matrix m n α) (f : αβ) (hf : ∀ (a : α), f a = a) :
A.map f = A
@[simp]
theorem Matrix.nnnorm_transpose {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] (A : Matrix m n α) :
A.transpose‖₊ = A‖₊
@[simp]
theorem Matrix.norm_transpose {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] (A : Matrix m n α) :
A.transpose = A
@[simp]
theorem Matrix.nnnorm_conjTranspose {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] [] (A : Matrix m n α) :
A.conjTranspose‖₊ = A‖₊
@[simp]
theorem Matrix.norm_conjTranspose {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] [] (A : Matrix m n α) :
A.conjTranspose = A
instance Matrix.instNormedStarGroup {m : Type u_3} {α : Type u_5} [] [] [] :
Equations
• =
@[simp]
theorem Matrix.nnnorm_col {m : Type u_3} {α : Type u_5} {ι : Type u_7} [] [] (v : mα) :
@[simp]
theorem Matrix.norm_col {m : Type u_3} {α : Type u_5} {ι : Type u_7} [] [] (v : mα) :
@[simp]
theorem Matrix.nnnorm_row {n : Type u_4} {α : Type u_5} {ι : Type u_7} [] [] (v : nα) :
@[simp]
theorem Matrix.norm_row {n : Type u_4} {α : Type u_5} {ι : Type u_7} [] [] (v : nα) :
@[simp]
theorem Matrix.nnnorm_diagonal {n : Type u_4} {α : Type u_5} [] [] (v : nα) :
@[simp]
theorem Matrix.norm_diagonal {n : Type u_4} {α : Type u_5} [] [] (v : nα) :
instance Matrix.instNormOneClassOfNonempty {n : Type u_4} {α : Type u_5} [] [] [] [One α] [] :

Note this is safe as an instance as it carries no data.

Equations
• =
def Matrix.normedAddCommGroup {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] :

Normed group instance (using sup norm of sup norm) for matrices over a normed group. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations
Instances For
theorem Matrix.boundedSMul {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] [Module R α] [] :
BoundedSMul R (Matrix m n α)

This applies to the sup norm of sup norm.

def Matrix.normedSpace {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] [] :
NormedSpace R (Matrix m n α)

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.

Equations
• Matrix.normedSpace = Pi.normedSpace
Instances For

### The $L_\infty$ operator norm #

This section defines the matrix norm $\|A\|_\infty = \operatorname{sup}_i (\sum_j \|A_{ij}\|)$.

Note that this is equivalent to the operator norm, considering $A$ as a linear map between two $L^\infty$ spaces.

def Matrix.linftyOpSeminormedAddCommGroup {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] :

Seminormed group instance (using sup norm of L1 norm) for matrices over a seminormed group. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations
Instances For
def Matrix.linftyOpNormedAddCommGroup {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] :

Normed group instance (using sup norm of L1 norm) for matrices over a normed ring. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations
Instances For
theorem Matrix.linftyOpBoundedSMul {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] [Module R α] [] :
BoundedSMul R (Matrix m n α)

This applies to the sup norm of L1 norm.

def Matrix.linftyOpNormedSpace {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] [] :
NormedSpace R (Matrix m n α)

Normed space instance (using sup norm of L1 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.

Equations
• Matrix.linftyOpNormedSpace = inferInstance
Instances For
theorem Matrix.linfty_opNorm_def {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] (A : Matrix m n α) :
A = (Finset.univ.sup fun (i : m) => j : n, A i j‖₊)
@[deprecated Matrix.linfty_opNorm_def]
theorem Matrix.linfty_op_norm_def {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] (A : Matrix m n α) :
A = (Finset.univ.sup fun (i : m) => j : n, A i j‖₊)

Alias of Matrix.linfty_opNorm_def.

theorem Matrix.linfty_opNNNorm_def {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] (A : Matrix m n α) :
A‖₊ = Finset.univ.sup fun (i : m) => j : n, A i j‖₊
@[deprecated Matrix.linfty_opNNNorm_def]
theorem Matrix.linfty_op_nnnorm_def {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] (A : Matrix m n α) :
A‖₊ = Finset.univ.sup fun (i : m) => j : n, A i j‖₊

Alias of Matrix.linfty_opNNNorm_def.

@[simp]
theorem Matrix.linfty_opNNNorm_col {m : Type u_3} {α : Type u_5} {ι : Type u_7} [] [] (v : mα) :
@[deprecated Matrix.linfty_opNNNorm_col]
theorem Matrix.linfty_op_nnnorm_col {m : Type u_3} {α : Type u_5} {ι : Type u_7} [] [] (v : mα) :

Alias of Matrix.linfty_opNNNorm_col.

@[simp]
theorem Matrix.linfty_opNorm_col {m : Type u_3} {α : Type u_5} {ι : Type u_7} [] [] (v : mα) :
@[deprecated Matrix.linfty_opNorm_col]
theorem Matrix.linfty_op_norm_col {m : Type u_3} {α : Type u_5} {ι : Type u_7} [] [] (v : mα) :

Alias of Matrix.linfty_opNorm_col.

@[simp]
theorem Matrix.linfty_opNNNorm_row {n : Type u_4} {α : Type u_5} {ι : Type u_7} [] [] (v : nα) :
‖₊ = i : n, v i‖₊
@[deprecated Matrix.linfty_opNNNorm_row]
theorem Matrix.linfty_op_nnnorm_row {n : Type u_4} {α : Type u_5} {ι : Type u_7} [] [] (v : nα) :
‖₊ = i : n, v i‖₊

Alias of Matrix.linfty_opNNNorm_row.

@[simp]
theorem Matrix.linfty_opNorm_row {n : Type u_4} {α : Type u_5} {ι : Type u_7} [] [] (v : nα) :
= i : n, v i
@[deprecated Matrix.linfty_opNorm_row]
theorem Matrix.linfty_op_norm_row {n : Type u_4} {α : Type u_5} {ι : Type u_7} [] [] (v : nα) :
= i : n, v i

Alias of Matrix.linfty_opNorm_row.

@[simp]
theorem Matrix.linfty_opNNNorm_diagonal {m : Type u_3} {α : Type u_5} [] [] (v : mα) :
@[deprecated Matrix.linfty_opNNNorm_diagonal]
theorem Matrix.linfty_op_nnnorm_diagonal {m : Type u_3} {α : Type u_5} [] [] (v : mα) :

Alias of Matrix.linfty_opNNNorm_diagonal.

@[simp]
theorem Matrix.linfty_opNorm_diagonal {m : Type u_3} {α : Type u_5} [] [] (v : mα) :
@[deprecated Matrix.linfty_opNorm_diagonal]
theorem Matrix.linfty_op_norm_diagonal {m : Type u_3} {α : Type u_5} [] [] (v : mα) :

Alias of Matrix.linfty_opNorm_diagonal.

theorem Matrix.linfty_opNNNorm_mul {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] (A : Matrix l m α) (B : Matrix m n α) :
@[deprecated Matrix.linfty_opNNNorm_mul]
theorem Matrix.linfty_op_nnnorm_mul {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] (A : Matrix l m α) (B : Matrix m n α) :

Alias of Matrix.linfty_opNNNorm_mul.

theorem Matrix.linfty_opNorm_mul {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] (A : Matrix l m α) (B : Matrix m n α) :
@[deprecated Matrix.linfty_opNorm_mul]
theorem Matrix.linfty_op_norm_mul {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] (A : Matrix l m α) (B : Matrix m n α) :

Alias of Matrix.linfty_opNorm_mul.

theorem Matrix.linfty_opNNNorm_mulVec {l : Type u_2} {m : Type u_3} {α : Type u_5} [] [] (A : Matrix l m α) (v : mα) :
@[deprecated Matrix.linfty_opNNNorm_mulVec]
theorem Matrix.linfty_op_nnnorm_mulVec {l : Type u_2} {m : Type u_3} {α : Type u_5} [] [] (A : Matrix l m α) (v : mα) :

Alias of Matrix.linfty_opNNNorm_mulVec.

theorem Matrix.linfty_opNorm_mulVec {l : Type u_2} {m : Type u_3} {α : Type u_5} [] [] (A : Matrix l m α) (v : mα) :
A.mulVec v A * v
@[deprecated Matrix.linfty_opNorm_mulVec]
theorem Matrix.linfty_op_norm_mulVec {l : Type u_2} {m : Type u_3} {α : Type u_5} [] [] (A : Matrix l m α) (v : mα) :
A.mulVec v A * v

Alias of Matrix.linfty_opNorm_mulVec.

Seminormed non-unital ring instance (using sup norm of L1 norm) for matrices over a semi normed non-unital ring. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations
• Matrix.linftyOpNonUnitalSemiNormedRing = let __src := Matrix.linftyOpSeminormedAddCommGroup; let __src_1 := Matrix.instNonUnitalRing;
Instances For
instance Matrix.linfty_opNormOneClass {n : Type u_4} {α : Type u_5} [] [] [] [] [] :

The L₁-L∞ norm preserves one on non-empty matrices. Note this is safe as an instance, as it carries no data.

Equations
• =
def Matrix.linftyOpSemiNormedRing {n : Type u_4} {α : Type u_5} [] [] [] :

Seminormed ring instance (using sup norm of L1 norm) for matrices over a semi normed ring. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations
• Matrix.linftyOpSemiNormedRing = let __src := Matrix.linftyOpNonUnitalSemiNormedRing; let __src_1 := Matrix.instRing;
Instances For

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.

Equations
• Matrix.linftyOpNonUnitalNormedRing = let __src := Matrix.linftyOpNonUnitalSemiNormedRing;
Instances For
def Matrix.linftyOpNormedRing {n : Type u_4} {α : Type u_5} [] [] [] :

Normed ring instance (using sup norm of L1 norm) for matrices over a normed ring. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations
• Matrix.linftyOpNormedRing = let __src := Matrix.linftyOpSemiNormedRing;
Instances For
def Matrix.linftyOpNormedAlgebra {R : Type u_1} {n : Type u_4} {α : Type u_5} [] [] [] [] [] :

Normed algebra instance (using sup norm of L1 norm) for matrices over a normed algebra. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations
• Matrix.linftyOpNormedAlgebra = let __src := Matrix.linftyOpNormedSpace; let __src_1 := Matrix.instAlgebra;
Instances For

For a matrix over a field, the norm defined in this section agrees with the operator norm on ContinuousLinearMaps between function types (which have the infinity norm).

theorem Matrix.linfty_opNNNorm_eq_opNNNorm {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] (A : Matrix m n α) :
A‖₊ = { toLinearMap := A.mulVecLin, cont := }‖₊
@[deprecated Matrix.linfty_opNNNorm_eq_opNNNorm]
theorem Matrix.linfty_op_nnnorm_eq_op_nnnorm {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] (A : Matrix m n α) :
A‖₊ = { toLinearMap := A.mulVecLin, cont := }‖₊

Alias of Matrix.linfty_opNNNorm_eq_opNNNorm.

theorem Matrix.linfty_opNorm_eq_opNorm {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] (A : Matrix m n α) :
A = { toLinearMap := A.mulVecLin, cont := }
@[deprecated Matrix.linfty_opNorm_eq_opNorm]
theorem Matrix.linfty_op_norm_eq_op_norm {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] (A : Matrix m n α) :
A = { toLinearMap := A.mulVecLin, cont := }

Alias of Matrix.linfty_opNorm_eq_opNorm.

@[simp]
theorem Matrix.linfty_opNNNorm_toMatrix {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] [] (f : (nα) →L[α] mα) :
LinearMap.toMatrix' f‖₊ = f‖₊
@[deprecated Matrix.linfty_opNNNorm_toMatrix]
theorem Matrix.linfty_op_nnnorm_toMatrix {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] [] (f : (nα) →L[α] mα) :
LinearMap.toMatrix' f‖₊ = f‖₊

Alias of Matrix.linfty_opNNNorm_toMatrix.

@[simp]
theorem Matrix.linfty_opNorm_toMatrix {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] [] (f : (nα) →L[α] mα) :
LinearMap.toMatrix' f = f
@[deprecated Matrix.linfty_opNorm_toMatrix]
theorem Matrix.linfty_op_norm_toMatrix {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] [] (f : (nα) →L[α] mα) :
LinearMap.toMatrix' f = f

Alias of Matrix.linfty_opNorm_toMatrix.

### The Frobenius norm #

This is defined as $\|A\| = \sqrt{\sum_{i,j} \|A_{ij}\|^2}$. When the matrix is over the real or complex numbers, this norm is submultiplicative.

def Matrix.frobeniusSeminormedAddCommGroup {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] :

Seminormed group instance (using frobenius norm) for matrices over a seminormed group. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations
Instances For
def Matrix.frobeniusNormedAddCommGroup {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] :

Normed group instance (using frobenius norm) for matrices over a normed group. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations
Instances For
theorem Matrix.frobeniusBoundedSMul {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] [Module R α] [] :
BoundedSMul R (Matrix m n α)

This applies to the frobenius norm.

def Matrix.frobeniusNormedSpace {R : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] [] :
NormedSpace R (Matrix m n α)

Normed space instance (using 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.

Equations
• Matrix.frobeniusNormedSpace = inferInstance
Instances For
theorem Matrix.frobenius_nnnorm_def {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] (A : Matrix m n α) :
A‖₊ = (i : m, j : n, A i j‖₊ ^ 2) ^ (1 / 2)
theorem Matrix.frobenius_norm_def {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] (A : Matrix m n α) :
A = (i : m, j : n, A i j ^ 2) ^ (1 / 2)
@[simp]
theorem Matrix.frobenius_nnnorm_map_eq {m : Type u_3} {n : Type u_4} {α : Type u_5} {β : Type u_6} [] [] (A : Matrix m n α) (f : αβ) (hf : ∀ (a : α), f a‖₊ = a‖₊) :
@[simp]
theorem Matrix.frobenius_norm_map_eq {m : Type u_3} {n : Type u_4} {α : Type u_5} {β : Type u_6} [] [] (A : Matrix m n α) (f : αβ) (hf : ∀ (a : α), f a = a) :
A.map f = A
@[simp]
theorem Matrix.frobenius_nnnorm_transpose {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] (A : Matrix m n α) :
A.transpose‖₊ = A‖₊
@[simp]
theorem Matrix.frobenius_norm_transpose {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] (A : Matrix m n α) :
A.transpose = A
@[simp]
theorem Matrix.frobenius_nnnorm_conjTranspose {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] [] (A : Matrix m n α) :
A.conjTranspose‖₊ = A‖₊
@[simp]
theorem Matrix.frobenius_norm_conjTranspose {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] [] (A : Matrix m n α) :
A.conjTranspose = A
instance Matrix.frobenius_normedStarGroup {m : Type u_3} {α : Type u_5} [] [] [] :
Equations
• =
@[simp]
theorem Matrix.frobenius_norm_row {m : Type u_3} {α : Type u_5} {ι : Type u_7} [] [] (v : mα) :
= (WithLp.equiv 2 (mα)).symm v
@[simp]
theorem Matrix.frobenius_nnnorm_row {m : Type u_3} {α : Type u_5} {ι : Type u_7} [] [] (v : mα) :
‖₊ = (WithLp.equiv 2 (mα)).symm v‖₊
@[simp]
theorem Matrix.frobenius_norm_col {n : Type u_4} {α : Type u_5} {ι : Type u_7} [] [] (v : nα) :
= (WithLp.equiv 2 (nα)).symm v
@[simp]
theorem Matrix.frobenius_nnnorm_col {n : Type u_4} {α : Type u_5} {ι : Type u_7} [] [] (v : nα) :
‖₊ = (WithLp.equiv 2 (nα)).symm v‖₊
@[simp]
theorem Matrix.frobenius_nnnorm_diagonal {n : Type u_4} {α : Type u_5} [] [] (v : nα) :
= (WithLp.equiv 2 (nα)).symm v‖₊
@[simp]
theorem Matrix.frobenius_norm_diagonal {n : Type u_4} {α : Type u_5} [] [] (v : nα) :
= (WithLp.equiv 2 (nα)).symm v
theorem Matrix.frobenius_nnnorm_one {n : Type u_4} {α : Type u_5} [] [] [One α] :
1‖₊ = NNReal.sqrt () * 1‖₊
theorem Matrix.frobenius_nnnorm_mul {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] [] (A : Matrix l m α) (B : Matrix m n α) :
theorem Matrix.frobenius_norm_mul {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [] [] [] [] (A : Matrix l m α) (B : Matrix m n α) :
def Matrix.frobeniusNormedRing {m : Type u_3} {α : Type u_5} [] [] [] :

Normed ring instance (using frobenius norm) for matrices over ℝ or ℂ. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations
• Matrix.frobeniusNormedRing = let __src := Matrix.frobeniusSeminormedAddCommGroup; let __src_1 := Matrix.instRing;
Instances For
def Matrix.frobeniusNormedAlgebra {R : Type u_1} {m : Type u_3} {α : Type u_5} [] [] [] [] [] :

Normed algebra instance (using frobenius norm) for matrices over ℝ or ℂ. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Equations
• Matrix.frobeniusNormedAlgebra = let __src := Matrix.frobeniusNormedSpace; let __src_1 := Matrix.instAlgebra;
Instances For