# mathlib3documentation

linear_algebra.matrix.hermitian

# Hermitian matrices #

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

This file defines hermitian matrices and some basic results about them.

See also is_self_adjoint, which generalizes this definition to other star rings.

## Main definition #

• matrix.is_hermitian : a matrix A : matrix n n α is hermitian if Aᴴ = A.

## Tags #

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

A matrix is hermitian if it is equal to its conjugate transpose. On the reals, this definition captures symmetric matrices.

Equations
theorem matrix.is_hermitian.eq {α : Type u_1} {n : Type u_4} [has_star α] {A : n α} (h : A.is_hermitian) :
@[protected]
theorem matrix.is_hermitian.is_self_adjoint {α : Type u_1} {n : Type u_4} [has_star α] {A : n α} (h : A.is_hermitian) :
@[ext]
theorem matrix.is_hermitian.ext {α : Type u_1} {n : Type u_4} [has_star α] {A : n α} :
( (i j : n), has_star.star (A j i) = A i j) A.is_hermitian
theorem matrix.is_hermitian.apply {α : Type u_1} {n : Type u_4} [has_star α] {A : n α} (h : A.is_hermitian) (i j : n) :
has_star.star (A j i) = A i j
theorem matrix.is_hermitian.ext_iff {α : Type u_1} {n : Type u_4} [has_star α] {A : n α} :
A.is_hermitian (i j : n), has_star.star (A j i) = A i j
@[simp]
theorem matrix.is_hermitian.map {α : Type u_1} {β : Type u_2} {n : Type u_4} [has_star α] [has_star β] {A : n α} (h : A.is_hermitian) (f : α β)  :
theorem matrix.is_hermitian.transpose {α : Type u_1} {n : Type u_4} [has_star α] {A : n α} (h : A.is_hermitian) :
@[simp]
theorem matrix.is_hermitian_transpose_iff {α : Type u_1} {n : Type u_4} [has_star α] (A : n α) :
theorem matrix.is_hermitian.conj_transpose {α : Type u_1} {n : Type u_4} [has_star α] {A : n α} (h : A.is_hermitian) :
@[simp]
theorem matrix.is_hermitian.submatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [has_star α] {A : n α} (h : A.is_hermitian) (f : m n) :
@[simp]
theorem matrix.is_hermitian_submatrix_equiv {α : Type u_1} {m : Type u_3} {n : Type u_4} [has_star α] {A : n α} (e : m n) :
@[simp]
theorem matrix.is_hermitian_conj_transpose_iff {α : Type u_1} {n : Type u_4} (A : n α) :
theorem matrix.is_hermitian.from_blocks {α : Type u_1} {m : Type u_3} {n : Type u_4} {A : m α} {B : n α} {C : m α} {D : n α} (hA : A.is_hermitian) (hBC : B.conj_transpose = C) (hD : D.is_hermitian) :

A block matrix A.from_blocks B C D is hermitian, if A and D are hermitian and Bᴴ = C.

theorem matrix.is_hermitian_from_blocks_iff {α : Type u_1} {m : Type u_3} {n : Type u_4} {A : m α} {B : n α} {C : m α} {D : n α} :

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

theorem matrix.is_hermitian_diagonal_of_self_adjoint {α : Type u_1} {n : Type u_4} [add_monoid α] [decidable_eq n] (v : n α) (h : is_self_adjoint v) :

A diagonal matrix is hermitian if the entries are self-adjoint

@[simp]
theorem matrix.is_hermitian_diagonal {α : Type u_1} {n : Type u_4} [add_monoid α] [decidable_eq n] (v : n α) :

A diagonal matrix is hermitian if the entries have the trivial star operation (such as on the reals).

@[simp]
theorem matrix.is_hermitian_zero {α : Type u_1} {n : Type u_4} [add_monoid α]  :
@[simp]
theorem matrix.is_hermitian.add {α : Type u_1} {n : Type u_4} [add_monoid α] {A B : n α} (hA : A.is_hermitian) (hB : B.is_hermitian) :
theorem matrix.is_hermitian_add_transpose_self {α : Type u_1} {n : Type u_4} (A : n α) :
theorem matrix.is_hermitian_transpose_add_self {α : Type u_1} {n : Type u_4} (A : n α) :
@[simp]
theorem matrix.is_hermitian.neg {α : Type u_1} {n : Type u_4} [add_group α] {A : n α} (h : A.is_hermitian) :
@[simp]
theorem matrix.is_hermitian.sub {α : Type u_1} {n : Type u_4} [add_group α] {A B : n α} (hA : A.is_hermitian) (hB : B.is_hermitian) :
theorem matrix.is_hermitian_mul_conj_transpose_self {α : Type u_1} {m : Type u_3} {n : Type u_4} [star_ring α] [fintype n] (A : n α) :

Note this is more general than is_self_adjoint.mul_star_self as B can be rectangular.

theorem matrix.is_hermitian_transpose_mul_self {α : Type u_1} {m : Type u_3} {n : Type u_4} [star_ring α] [fintype m] (A : n α) :

Note this is more general than is_self_adjoint.star_mul_self as B can be rectangular.

theorem matrix.is_hermitian_conj_transpose_mul_mul {α : Type u_1} {m : Type u_3} {n : Type u_4} [star_ring α] [fintype m] {A : m α} (B : n α) (hA : A.is_hermitian) :

Note this is more general than is_self_adjoint.conjugate' as B can be rectangular.

theorem matrix.is_hermitian_mul_mul_conj_transpose {α : Type u_1} {m : Type u_3} {n : Type u_4} [star_ring α] [fintype m] {A : m α} (B : m α) (hA : A.is_hermitian) :

Note this is more general than is_self_adjoint.conjugate as B can be rectangular.

@[simp]
theorem matrix.is_hermitian_one {α : Type u_1} {n : Type u_4} [semiring α] [star_ring α] [decidable_eq n] :

Note this is more general for matrices than is_self_adjoint_one as it does not require fintype n, which is necessary for monoid (matrix n n R).

theorem matrix.is_hermitian.inv {α : Type u_1} {m : Type u_3} [comm_ring α] [star_ring α] [fintype m] [decidable_eq m] {A : m α} (hA : A.is_hermitian) :
@[simp]
theorem matrix.is_hermitian_inv {α : Type u_1} {m : Type u_3} [comm_ring α] [star_ring α] [fintype m] [decidable_eq m] (A : m α) [invertible A] :
theorem matrix.is_hermitian.adjugate {α : Type u_1} {m : Type u_3} [comm_ring α] [star_ring α] [fintype m] [decidable_eq m] {A : m α} (hA : A.is_hermitian) :
theorem matrix.is_hermitian.coe_re_apply_self {α : Type u_1} {n : Type u_4} [is_R_or_C α] {A : n α} (h : A.is_hermitian) (i : n) :
(is_R_or_C.re (A i i)) = A i i

The diagonal elements of a complex hermitian matrix are real.

theorem matrix.is_hermitian.coe_re_diag {α : Type u_1} {n : Type u_4} [is_R_or_C α] {A : n α} (h : A.is_hermitian) :
(λ (i : n), (is_R_or_C.re (A.diag i))) = A.diag

The diagonal elements of a complex hermitian matrix are real.

theorem matrix.is_hermitian_iff_is_symmetric {α : Type u_1} {n : Type u_4} [is_R_or_C α] [fintype n] [decidable_eq n] {A : n α} :

A matrix is hermitian iff the corresponding linear map is self adjoint.