Documentation

Mathlib.LinearAlgebra.Matrix.IsDiag

Diagonal matrices #

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

Main results #

Tags #

diag, diagonal, matrix

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

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

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

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

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

    Matrix.IsDiag.diagonal_diag as an iff.

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

    Every matrix indexed by a subsingleton is diagonal.

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

    Every zero matrix is diagonal.

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

    Every identity matrix is diagonal.

    source
    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
    source
    theorem Matrix.IsDiag.neg {α : Type u_1} {n : Type u_4} [SubtractionMonoid α] {A : Matrix n n α} (ha : A.IsDiag) :
    (-A).IsDiag
    source
    @[simp]
    theorem Matrix.isDiag_neg_iff {α : Type u_1} {n : Type u_4} [SubtractionMonoid α] {A : Matrix n n α} :
    (-A).IsDiag ↔ A.IsDiag
    source
    theorem Matrix.IsDiag.add {α : Type u_1} {n : Type u_4} [AddZeroClass α] {A B : Matrix n n α} (ha : A.IsDiag) (hb : B.IsDiag) :
    (A + B).IsDiag
    source
    theorem Matrix.IsDiag.sub {α : Type u_1} {n : Type u_4} [SubtractionMonoid α] {A B : Matrix n n α} (ha : A.IsDiag) (hb : B.IsDiag) :
    (A - B).IsDiag
    source
    theorem Matrix.IsDiag.smul {α : Type u_1} {R : Type u_3} {n : Type u_4} [Zero α] [SMulZeroClass R α] (k : R) {A : Matrix n n α} (ha : A.IsDiag) :
    (k • A).IsDiag
    source
    @[simp]
    theorem Matrix.isDiag_smul_one {α : Type u_1} (n : Type u_6) [MulZeroOneClass α] [DecidableEq n] (k : α) :
    (k • 1).IsDiag
    source
    theorem Matrix.IsDiag.transpose {α : Type u_1} {n : Type u_4} [Zero α] {A : Matrix n n α} (ha : A.IsDiag) :
    A.transpose.IsDiag
    source
    @[simp]
    theorem Matrix.isDiag_transpose_iff {α : Type u_1} {n : Type u_4} [Zero α] {A : Matrix n n α} :
    A.transpose.IsDiag ↔ A.IsDiag
    source
    theorem Matrix.IsDiag.conjTranspose {α : Type u_1} {n : Type u_4} [NonUnitalNonAssocSemiring α] [StarRing α] {A : Matrix n n α} (ha : A.IsDiag) :
    A.conjTranspose.IsDiag
    source
    @[simp]
    theorem Matrix.isDiag_conjTranspose_iff {α : Type u_1} {n : Type u_4} [NonUnitalNonAssocSemiring α] [StarRing α] {A : Matrix n n α} :
    A.conjTranspose.IsDiag ↔ A.IsDiag
    source
    theorem Matrix.IsDiag.submatrix {α : Type u_1} {n : Type u_4} {m : Type u_5} [Zero α] {A : Matrix n n α} (ha : A.IsDiag) {f : m → n} (hf : Function.Injective f) :
    (A.submatrix f f).IsDiag
    source
    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 : A.IsDiag) (hB : B.IsDiag) :
    (kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B).IsDiag

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

    source
    theorem Matrix.IsDiag.isSymm {α : Type u_1} {n : Type u_4} [Zero α] {A : Matrix n n α} (h : A.IsDiag) :
    A.IsSymm
    source
    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) :
    (Matrix.fromBlocks A 0 0 D).IsDiag

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

    source
    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 α} :
    (fromBlocks A B C D).IsDiag ↔ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag

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

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

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

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