mathlib3documentation

linear_algebra.matrix.is_diag

Diagonal matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main results #

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

Tags #

diag, diagonal, matrix

def matrix.is_diag {α : Type u_1} {n : Type u_4} [has_zero α] (A : n α) :
Prop

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

Equations
@[simp]
theorem matrix.is_diag_diagonal {α : Type u_1} {n : Type u_4} [has_zero α] [decidable_eq n] (d : n α) :
theorem matrix.is_diag.diagonal_diag {α : Type u_1} {n : Type u_4} [has_zero α] [decidable_eq n] {A : n α} (h : A.is_diag) :

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

theorem matrix.is_diag_iff_diagonal_diag {α : Type u_1} {n : Type u_4} [has_zero α] [decidable_eq n] (A : n α) :

matrix.is_diag.diagonal_diag as an iff.

theorem matrix.is_diag_of_subsingleton {α : Type u_1} {n : Type u_4} [has_zero α] [subsingleton n] (A : n α) :

Every matrix indexed by a subsingleton is diagonal.

@[simp]
theorem matrix.is_diag_zero {α : Type u_1} {n : Type u_4} [has_zero α] :

Every zero matrix is diagonal.

@[simp]
theorem matrix.is_diag_one {α : Type u_1} {n : Type u_4} [decidable_eq n] [has_zero α] [has_one α] :

Every identity matrix is diagonal.

theorem matrix.is_diag.map {α : Type u_1} {β : Type u_2} {n : Type u_4} [has_zero α] [has_zero β] {A : n α} (ha : A.is_diag) {f : α β} (hf : f 0 = 0) :
(A.map f).is_diag
theorem matrix.is_diag.neg {α : Type u_1} {n : Type u_4} [add_group α] {A : n α} (ha : A.is_diag) :
@[simp]
theorem matrix.is_diag_neg_iff {α : Type u_1} {n : Type u_4} [add_group α] {A : n α} :
theorem matrix.is_diag.add {α : Type u_1} {n : Type u_4} {A B : n α} (ha : A.is_diag) (hb : B.is_diag) :
(A + B).is_diag
theorem matrix.is_diag.sub {α : Type u_1} {n : Type u_4} [add_group α] {A B : n α} (ha : A.is_diag) (hb : B.is_diag) :
(A - B).is_diag
theorem matrix.is_diag.smul {α : Type u_1} {R : Type u_3} {n : Type u_4} [monoid R] [add_monoid α] [ α] (k : R) {A : n α} (ha : A.is_diag) :
(k A).is_diag
@[simp]
theorem matrix.is_diag_smul_one {α : Type u_1} (n : Type u_2) [semiring α] [decidable_eq n] (k : α) :
(k 1).is_diag
theorem matrix.is_diag.transpose {α : Type u_1} {n : Type u_4} [has_zero α] {A : n α} (ha : A.is_diag) :
@[simp]
theorem matrix.is_diag_transpose_iff {α : Type u_1} {n : Type u_4} [has_zero α] {A : n α} :
theorem matrix.is_diag.conj_transpose {α : Type u_1} {n : Type u_4} [semiring α] [star_ring α] {A : n α} (ha : A.is_diag) :
@[simp]
theorem matrix.is_diag_conj_transpose_iff {α : Type u_1} {n : Type u_4} [semiring α] [star_ring α] {A : n α} :
theorem matrix.is_diag.submatrix {α : Type u_1} {n : Type u_4} {m : Type u_5} [has_zero α] {A : n α} (ha : A.is_diag) {f : m n} (hf : function.injective f) :
theorem matrix.is_diag.kronecker {α : Type u_1} {n : Type u_4} {m : Type u_5} {A : m α} {B : n α} (hA : A.is_diag) (hB : B.is_diag) :

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

theorem matrix.is_diag.is_symm {α : Type u_1} {n : Type u_4} [has_zero α] {A : n α} (h : A.is_diag) :
theorem matrix.is_diag.from_blocks {α : Type u_1} {n : Type u_4} {m : Type u_5} [has_zero α] {A : m α} {D : n α} (ha : A.is_diag) (hd : D.is_diag) :
0 D).is_diag

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

theorem matrix.is_diag_from_blocks_iff {α : Type u_1} {n : Type u_4} {m : Type u_5} [has_zero α] {A : m α} {B : n α} {C : m α} {D : n α} :
C D).is_diag A.is_diag B = 0 C = 0 D.is_diag

This is the iff version of matrix.is_diag.from_blocks.

theorem matrix.is_diag.from_blocks_of_is_symm {α : Type u_1} {n : Type u_4} {m : Type u_5} [has_zero α] {A : m α} {C : m α} {D : n α} (h : C D).is_symm) (ha : A.is_diag) (hd : D.is_diag) :
C D).is_diag

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