Documentation

Mathlib.LinearAlgebra.Matrix.IsDiag

Diagonal matrices #

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

Main results #

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 α] [DecidableEq n] (d : nα) :
    theorem Matrix.IsDiag.diagonal_diag {α : Type u_1} {n : Type u_4} [Zero α] [DecidableEq n] {A : Matrix n n α} (h : Matrix.IsDiag A) :

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

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

    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} [DecidableEq n] [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 : Matrix.IsDiag A) {f : αβ} (hf : f 0 = 0) :
    theorem Matrix.IsDiag.neg {α : Type u_1} {n : Type u_4} [AddGroup α] {A : Matrix n n α} (ha : Matrix.IsDiag A) :
    @[simp]
    theorem Matrix.isDiag_neg_iff {α : Type u_1} {n : Type u_4} [AddGroup α] {A : Matrix n n α} :
    theorem Matrix.IsDiag.add {α : Type u_1} {n : Type u_4} [AddZeroClass α] {A : Matrix n n α} {B : Matrix n n α} (ha : Matrix.IsDiag A) (hb : Matrix.IsDiag B) :
    theorem Matrix.IsDiag.sub {α : Type u_1} {n : Type u_4} [AddGroup α] {A : Matrix n n α} {B : Matrix n n α} (ha : Matrix.IsDiag A) (hb : Matrix.IsDiag B) :
    theorem Matrix.IsDiag.smul {α : Type u_1} {R : Type u_3} {n : Type u_4} [Monoid R] [AddMonoid α] [DistribMulAction R α] (k : R) {A : Matrix n n α} (ha : Matrix.IsDiag A) :
    @[simp]
    theorem Matrix.isDiag_smul_one {α : Type u_1} (n : Type u_6) [Semiring α] [DecidableEq n] (k : α) :
    theorem Matrix.IsDiag.transpose {α : Type u_1} {n : Type u_4} [Zero α] {A : Matrix n n α} (ha : Matrix.IsDiag A) :
    @[simp]
    theorem Matrix.isDiag_transpose_iff {α : Type u_1} {n : Type u_4} [Zero α] {A : Matrix n n α} :
    theorem Matrix.IsDiag.conjTranspose {α : Type u_1} {n : Type u_4} [Semiring α] [StarRing α] {A : Matrix n n α} (ha : Matrix.IsDiag A) :
    theorem Matrix.IsDiag.submatrix {α : Type u_1} {n : Type u_4} {m : Type u_5} [Zero α] {A : Matrix n n α} (ha : Matrix.IsDiag A) {f : mn} (hf : Function.Injective f) :
    theorem Matrix.IsDiag.kronecker {α : Type u_1} {n : Type u_4} {m : Type u_5} [MulZeroClass α] {A : Matrix m m α} {B : Matrix n n α} (hA : Matrix.IsDiag A) (hB : Matrix.IsDiag B) :
    Matrix.IsDiag (Matrix.kroneckerMap (fun (x x_1 : α) => x * x_1) A B)

    (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 : Matrix.IsDiag A) :
    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 : Matrix.IsDiag A) (hd : Matrix.IsDiag D) :

    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 α} :

    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 : Matrix.IsSymm (Matrix.fromBlocks A 0 C D)) (ha : Matrix.IsDiag A) (hd : Matrix.IsDiag D) :

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