mathlib documentation

linear_algebra.matrix.is_diag

Diagonal matrices #

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

Main results #

Tags #

diag, diagonal, matrix

def matrix.is_diag {α : Type u_1} {n : Type u_4} [has_zero α] (A : matrix n 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.exists_diagonal {α : Type u_1} {n : Type u_4} [has_zero α] [decidable_eq n] {A : matrix n n α} (h : A.is_diag) :
∃ (d : n → α), matrix.diagonal d = A

Diagonal matrices are generated by matrix.diagonal.

theorem matrix.is_diag_iff_exists_diagonal {α : Type u_1} {n : Type u_4} [has_zero α] [decidable_eq n] (A : matrix n n α) :
A.is_diag ∃ (d : n → α), matrix.diagonal d = A

matrix.is_diag.exists_diagonal as an iff.

theorem matrix.is_diag_of_subsingleton {α : Type u_1} {n : Type u_4} [has_zero α] [subsingleton n] (A : matrix n 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 : matrix n 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 : matrix n n α} (ha : A.is_diag) :
@[simp]
theorem matrix.is_diag_neg_iff {α : Type u_1} {n : Type u_4} [add_group α] {A : matrix n n α} :
theorem matrix.is_diag.add {α : Type u_1} {n : Type u_4} [add_zero_class α] {A B : matrix n 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 : matrix n 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 α] [distrib_mul_action R α] (k : R) {A : matrix n 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 : matrix n n α} (ha : A.is_diag) :
@[simp]
theorem matrix.is_diag_transpose_iff {α : Type u_1} {n : Type u_4} [has_zero α] {A : matrix n n α} :
theorem matrix.is_diag.conj_transpose {α : Type u_1} {n : Type u_4} [semiring α] [star_ring α] {A : matrix n n α} (ha : A.is_diag) :
@[simp]
theorem matrix.is_diag_conj_transpose_iff {α : Type u_1} {n : Type u_4} [semiring α] [star_ring α] {A : matrix n n α} :
theorem matrix.is_diag.minor {α : Type u_1} {n : Type u_4} {m : Type u_5} [has_zero α] {A : matrix n n α} (ha : A.is_diag) {f : m → n} (hf : function.injective f) :
(A.minor f f).is_diag
theorem matrix.is_diag.kronecker {α : Type u_1} {n : Type u_4} {m : Type u_5} [mul_zero_class α] {A : matrix m m α} {B : matrix n 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 : matrix n 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 : matrix m m α} {D : matrix n n α} (ha : A.is_diag) (hd : 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 : matrix m m α} {B : matrix m n α} {C : matrix n m α} {D : matrix n n α} :
(A.from_blocks B 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 : matrix m m α} {C : matrix n m α} {D : matrix n n α} (h : (A.from_blocks 0 C D).is_symm) (ha : A.is_diag) (hd : 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.

theorem matrix.mul_transpose_self_is_diag_iff_has_orthogonal_rows {α : Type u_1} {n : Type u_4} {m : Type u_5} [fintype n] [has_mul α] [add_comm_monoid α] {A : matrix m n α} :
theorem matrix.transpose_mul_self_is_diag_iff_has_orthogonal_cols {α : Type u_1} {n : Type u_4} {m : Type u_5} [fintype m] [has_mul α] [add_comm_monoid α] {A : matrix m n α} :