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

    Every matrix indexed by a subsingleton is diagonal.

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

    Every zero matrix is diagonal.

    source
    @[simp]
    theorem Matrix.isDiag_one {α : Type u_1} {n : Type u_4} [DecidableEq n] [Zero α] [One α] :
    Matrix.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 : Matrix.IsDiag A) {f : α → β} (hf : f 0 = 0) :
    Matrix.IsDiag (Matrix.map A f)
    source
    theorem Matrix.IsDiag.neg {α : Type u_1} {n : Type u_4} [AddGroup α] {A : Matrix n n α} (ha : Matrix.IsDiag A) :
    Matrix.IsDiag (-A)
    source
    @[simp]
    theorem Matrix.isDiag_neg_iff {α : Type u_1} {n : Type u_4} [AddGroup α] {A : Matrix n n α} :
    Matrix.IsDiag (-A) ↔ Matrix.IsDiag A
    source
    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) :
    Matrix.IsDiag (A + B)
    source
    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) :
    Matrix.IsDiag (A - B)
    source
    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) :
    Matrix.IsDiag (k • A)
    source
    @[simp]
    theorem Matrix.isDiag_smul_one {α : Type u_1} (n : Type u_6) [Semiring α] [DecidableEq n] (k : α) :
    Matrix.IsDiag (k • 1)
    source
    theorem Matrix.IsDiag.transpose {α : Type u_1} {n : Type u_4} [Zero α] {A : Matrix n n α} (ha : Matrix.IsDiag A) :
    Matrix.IsDiag (Matrix.transpose A)
    source
    @[simp]
    theorem Matrix.isDiag_transpose_iff {α : Type u_1} {n : Type u_4} [Zero α] {A : Matrix n n α} :
    Matrix.IsDiag (Matrix.transpose A) ↔ Matrix.IsDiag A
    source
    theorem Matrix.IsDiag.conjTranspose {α : Type u_1} {n : Type u_4} [Semiring α] [StarRing α] {A : Matrix n n α} (ha : Matrix.IsDiag A) :
    Matrix.IsDiag (Matrix.conjTranspose A)
    source
    @[simp]
    theorem Matrix.isDiag_conjTranspose_iff {α : Type u_1} {n : Type u_4} [Semiring α] [StarRing α] {A : Matrix n n α} :
    Matrix.IsDiag (Matrix.conjTranspose A) ↔ Matrix.IsDiag A
    source
    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 : m → n} (hf : Function.Injective f) :
    Matrix.IsDiag (Matrix.submatrix A f f)
    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 : 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.

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

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

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

    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 α} :
    Matrix.IsDiag (A * Matrix.transpose A) ↔ Matrix.HasOrthogonalRows A
    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 α} :
    Matrix.IsDiag (Matrix.transpose A * A) ↔ Matrix.HasOrthogonalCols A