# Diagonal matrices #

This file contains the definition and basic results about diagonal matrices.

## Main results #

• Matrix.IsDiag: a proposition that states a given square matrix A is diagonal.

## Tags #

diag, diagonal, matrix

def Matrix.IsDiag {α : Type u_1} {n : Type u_4} [Zero α] (A : Matrix n n α) :

A.IsDiag means square matrix A is a diagonal matrix.

Equations
Instances For
@[simp]
theorem Matrix.isDiag_diagonal {α : Type u_1} {n : Type u_4} [Zero α] [] (d : nα) :
().IsDiag
theorem Matrix.IsDiag.diagonal_diag {α : Type u_1} {n : Type u_4} [Zero α] [] {A : Matrix n n α} (h : A.IsDiag) :

Diagonal matrices are generated by the Matrix.diagonal of their Matrix.diag.

theorem Matrix.isDiag_iff_diagonal_diag {α : Type u_1} {n : Type u_4} [Zero α] [] (A : Matrix n n α) :
A.IsDiag Matrix.diagonal A.diag = A

Matrix.IsDiag.diagonal_diag as an iff.

theorem Matrix.isDiag_of_subsingleton {α : Type u_1} {n : Type u_4} [Zero α] [] (A : Matrix n n α) :
A.IsDiag

Every matrix indexed by a subsingleton is diagonal.

@[simp]
theorem Matrix.isDiag_zero {α : Type u_1} {n : Type u_4} [Zero α] :

Every zero matrix is diagonal.

@[simp]
theorem Matrix.isDiag_one {α : Type u_1} {n : Type u_4} [] [Zero α] [One α] :

Every identity matrix is diagonal.

theorem Matrix.IsDiag.map {α : Type u_1} {β : Type u_2} {n : Type u_4} [Zero α] [Zero β] {A : Matrix n n α} (ha : A.IsDiag) {f : αβ} (hf : f 0 = 0) :
(A.map f).IsDiag
theorem Matrix.IsDiag.neg {α : Type u_1} {n : Type u_4} [] {A : Matrix n n α} (ha : A.IsDiag) :
(-A).IsDiag
@[simp]
theorem Matrix.isDiag_neg_iff {α : Type u_1} {n : Type u_4} [] {A : Matrix n n α} :
(-A).IsDiag A.IsDiag
theorem Matrix.IsDiag.add {α : Type u_1} {n : Type u_4} [] {A : Matrix n n α} {B : Matrix n n α} (ha : A.IsDiag) (hb : B.IsDiag) :
(A + B).IsDiag
theorem Matrix.IsDiag.sub {α : Type u_1} {n : Type u_4} [] {A : Matrix n n α} {B : Matrix n n α} (ha : A.IsDiag) (hb : B.IsDiag) :
(A - B).IsDiag
theorem Matrix.IsDiag.smul {α : Type u_1} {R : Type u_3} {n : Type u_4} [] [] [] (k : R) {A : Matrix n n α} (ha : A.IsDiag) :
(k A).IsDiag
@[simp]
theorem Matrix.isDiag_smul_one {α : Type u_1} (n : Type u_6) [] [] (k : α) :
(k 1).IsDiag
theorem Matrix.IsDiag.transpose {α : Type u_1} {n : Type u_4} [Zero α] {A : Matrix n n α} (ha : A.IsDiag) :
A.transpose.IsDiag
@[simp]
theorem Matrix.isDiag_transpose_iff {α : Type u_1} {n : Type u_4} [Zero α] {A : Matrix n n α} :
A.transpose.IsDiag A.IsDiag
theorem Matrix.IsDiag.conjTranspose {α : Type u_1} {n : Type u_4} [] [] {A : Matrix n n α} (ha : A.IsDiag) :
A.conjTranspose.IsDiag
@[simp]
theorem Matrix.isDiag_conjTranspose_iff {α : Type u_1} {n : Type u_4} [] [] {A : Matrix n n α} :
A.conjTranspose.IsDiag A.IsDiag
theorem Matrix.IsDiag.submatrix {α : Type u_1} {n : Type u_4} {m : Type u_5} [Zero α] {A : Matrix n n α} (ha : A.IsDiag) {f : mn} (hf : ) :
(A.submatrix f f).IsDiag
theorem Matrix.IsDiag.kronecker {α : Type u_1} {n : Type u_4} {m : Type u_5} [] {A : Matrix m m α} {B : Matrix n n α} (hA : A.IsDiag) (hB : B.IsDiag) :
(Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A B).IsDiag

(A ⊗ B).IsDiag if both A and B are diagonal.

theorem Matrix.IsDiag.isSymm {α : Type u_1} {n : Type u_4} [Zero α] {A : Matrix n n α} (h : A.IsDiag) :
A.IsSymm
theorem Matrix.IsDiag.fromBlocks {α : Type u_1} {n : Type u_4} {m : Type u_5} [Zero α] {A : Matrix m m α} {D : Matrix n n α} (ha : A.IsDiag) (hd : D.IsDiag) :
().IsDiag

The block matrix A.fromBlocks 0 0 D is diagonal if A and D are diagonal.

theorem Matrix.isDiag_fromBlocks_iff {α : Type u_1} {n : Type u_4} {m : Type u_5} [Zero α] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} :
().IsDiag A.IsDiag B = 0 C = 0 D.IsDiag

This is the iff version of Matrix.IsDiag.fromBlocks.

theorem Matrix.IsDiag.fromBlocks_of_isSymm {α : Type u_1} {n : Type u_4} {m : Type u_5} [Zero α] {A : Matrix m m α} {C : Matrix n m α} {D : Matrix n n α} (h : ().IsSymm) (ha : A.IsDiag) (hd : D.IsDiag) :
().IsDiag

A symmetric block matrix A.fromBlocks B C D is diagonal if A and D are diagonal and B is 0.

theorem Matrix.mul_transpose_self_isDiag_iff_hasOrthogonalRows {α : Type u_1} {n : Type u_4} {m : Type u_5} [] [Mul α] [] {A : Matrix m n α} :
(A * A.transpose).IsDiag A.HasOrthogonalRows
theorem Matrix.transpose_mul_self_isDiag_iff_hasOrthogonalCols {α : Type u_1} {n : Type u_4} {m : Type u_5} [] [Mul α] [] {A : Matrix m n α} :
(A.transpose * A).IsDiag A.HasOrthogonalCols