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

source

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

A.is_diag = ∀ ⦃i j : n⦄, i ≠ j → A i j = 0

source

@[simp]

theorem matrix.is_diag_diagonal {α : Type u_1} {n : Type u_4} [has_zero α] [decidable_eq n] (d : n → α) :

(matrix.diagonal d).is_diag

source

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

matrix.diagonal A.diag = A

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

source

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

A.is_diag ↔ matrix.diagonal A.diag = A

matrix.is_diag.diagonal_diag as an iff.

source

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

A.is_diag

Every matrix indexed by a subsingleton is diagonal.

source

@[simp]

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

0.is_diag

Every zero matrix is diagonal.

source

@[simp]

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

1.is_diag

Every identity matrix is diagonal.

source

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

source

theorem matrix.is_diag.neg {α : Type u_1} {n : Type u_4} [add_group α] {A : matrix n n α} (ha : A.is_diag) :

(-A).is_diag

source

@[simp]

theorem matrix.is_diag_neg_iff {α : Type u_1} {n : Type u_4} [add_group α] {A : matrix n n α} :

(-A).is_diag ↔ A.is_diag

source

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

source

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

source

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

source

@[simp]

theorem matrix.is_diag_smul_one {α : Type u_1} (n : Type u_2) [semiring α] [decidable_eq n] (k : α) :

(k • 1).is_diag

source

theorem matrix.is_diag.transpose {α : Type u_1} {n : Type u_4} [has_zero α] {A : matrix n n α} (ha : A.is_diag) :

A.transpose.is_diag

source

@[simp]

theorem matrix.is_diag_transpose_iff {α : Type u_1} {n : Type u_4} [has_zero α] {A : matrix n n α} :

A.transpose.is_diag ↔ A.is_diag

source

theorem matrix.is_diag.conj_transpose {α : Type u_1} {n : Type u_4} [semiring α] [star_ring α] {A : matrix n n α} (ha : A.is_diag) :

A.conj_transpose.is_diag

source

@[simp]

theorem matrix.is_diag_conj_transpose_iff {α : Type u_1} {n : Type u_4} [semiring α] [star_ring α] {A : matrix n n α} :

A.conj_transpose.is_diag ↔ A.is_diag

source

theorem matrix.is_diag.submatrix {α : 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.submatrix f f).is_diag

source

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) :

(matrix.kronecker_map has_mul.mul A B).is_diag

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

source

theorem matrix.is_diag.is_symm {α : Type u_1} {n : Type u_4} [has_zero α] {A : matrix n n α} (h : A.is_diag) :

A.is_symm

source

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) :

(matrix.from_blocks A 0 0 D).is_diag

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

source

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

(matrix.from_blocks A 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.

source

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 : (matrix.from_blocks A 0 C D).is_symm) (ha : A.is_diag) (hd : D.is_diag) :

(matrix.from_blocks A 0 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.

source

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

(A.mul A.transpose).is_diag ↔ A.has_orthogonal_rows

source

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

(A.transpose.mul A).is_diag ↔ A.has_orthogonal_cols