# Hermitian matrices #

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

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

## Main definition #

- `Matrix.IsHermitian` : a matrix `A : Matrix n n α` is Hermitian if `Aᴴ = A`.

## Tags #

self-adjoint matrix, hermitian matrix

source
def Matrix.IsHermitian {α : Type u_1} {n : Type u_4} [Star α] (A : Matrix n n α) :
Prop

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

Equations

- A.IsHermitian = (A.conjTranspose = A)

Instances For

source
instance Matrix.instDecidableIsHermitianOfEqConjTranspose {α : Type u_1} {n : Type u_4} [Star α] (A : Matrix n n α) [Decidable (A.conjTranspose = A)] :
Decidable A.IsHermitian
Equations

- A.instDecidableIsHermitianOfEqConjTranspose = inferInstanceAs (Decidable (A.conjTranspose = A))

source
theorem Matrix.IsHermitian.eq {α : Type u_1} {n : Type u_4} [Star α] {A : Matrix n n α} (h : A.IsHermitian) :
A.conjTranspose = A
source
theorem Matrix.isHermitian_iff_isSelfAdjoint {α : Type u_1} {n : Type u_4} [Star α] {A : Matrix n n α} :
A.IsHermitian ↔ IsSelfAdjoint A
source
theorem IsSelfAdjoint.isHermitian {α : Type u_1} {n : Type u_4} [Star α] {A : Matrix n n α} :
IsSelfAdjoint A → A.IsHermitian

Alias of the reverse direction of `Matrix.isHermitian_iff_isSelfAdjoint`.

source
theorem Matrix.IsHermitian.isSelfAdjoint {α : Type u_1} {n : Type u_4} [Star α] {A : Matrix n n α} :
A.IsHermitian → IsSelfAdjoint A

Alias of the forward direction of `Matrix.isHermitian_iff_isSelfAdjoint`.

source
theorem Matrix.IsHermitian.ext {α : Type u_1} {n : Type u_4} [Star α] {A : Matrix n n α} :
(∀ (i j : n), star (A j i) = A i j) → A.IsHermitian
source
theorem Matrix.IsHermitian.apply {α : Type u_1} {n : Type u_4} [Star α] {A : Matrix n n α} (h : A.IsHermitian) (i j : n) :
star (A j i) = A i j
source
theorem Matrix.IsHermitian.ext_iff {α : Type u_1} {n : Type u_4} [Star α] {A : Matrix n n α} :
A.IsHermitian ↔ ∀ (i j : n), star (A j i) = A i j
source
@[simp]
theorem Matrix.IsHermitian.map {α : Type u_1} {β : Type u_2} {n : Type u_4} [Star α] [Star β] {A : Matrix n n α} (h : A.IsHermitian) (f : α → β) (hf : Function.Semiconj f star star) :
(A.map f).IsHermitian
source
theorem Matrix.IsHermitian.transpose {α : Type u_1} {n : Type u_4} [Star α] {A : Matrix n n α} (h : A.IsHermitian) :
A.transpose.IsHermitian
source
@[simp]
theorem Matrix.isHermitian_transpose_iff {α : Type u_1} {n : Type u_4} [Star α] (A : Matrix n n α) :
A.transpose.IsHermitian ↔ A.IsHermitian
source
theorem Matrix.IsHermitian.conjTranspose {α : Type u_1} {n : Type u_4} [Star α] {A : Matrix n n α} (h : A.IsHermitian) :
A.conjTranspose.IsHermitian
source
@[simp]
theorem Matrix.IsHermitian.submatrix {α : Type u_1} {m : Type u_3} {n : Type u_4} [Star α] {A : Matrix n n α} (h : A.IsHermitian) (f : m → n) :
(A.submatrix f f).IsHermitian
source
@[simp]
theorem Matrix.isHermitian_submatrix_equiv {α : Type u_1} {m : Type u_3} {n : Type u_4} [Star α] {A : Matrix n n α} (e : m ≃ n) :
(A.submatrix ⇑e ⇑e).IsHermitian ↔ A.IsHermitian
source
@[simp]
theorem Matrix.isHermitian_conjTranspose_iff {α : Type u_1} {n : Type u_4} [InvolutiveStar α] (A : Matrix n n α) :
A.conjTranspose.IsHermitian ↔ A.IsHermitian
source
theorem Matrix.IsHermitian.fromBlocks {α : Type u_1} {m : Type u_3} {n : Type u_4} [InvolutiveStar α] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} (hA : A.IsHermitian) (hBC : B.conjTranspose = C) (hD : D.IsHermitian) :
(Matrix.fromBlocks A B C D).IsHermitian

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

source
theorem Matrix.isHermitian_fromBlocks_iff {α : Type u_1} {m : Type u_3} {n : Type u_4} [InvolutiveStar α] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} :
(fromBlocks A B C D).IsHermitian ↔ A.IsHermitian ∧ B.conjTranspose = C ∧ C.conjTranspose = B ∧ D.IsHermitian

This is the `iff` version of `Matrix.IsHermitian.fromBlocks`.

source
theorem Matrix.isHermitian_diagonal_of_self_adjoint {α : Type u_1} {n : Type u_4} [AddMonoid α] [StarAddMonoid α] [DecidableEq n] (v : n → α) (h : IsSelfAdjoint v) :
(diagonal v).IsHermitian

A diagonal matrix is Hermitian if the entries are self-adjoint (as a vector)

source
theorem Matrix.isHermitian_diagonal_iff {α : Type u_1} {n : Type u_4} [AddMonoid α] [StarAddMonoid α] [DecidableEq n] {d : n → α} :
(diagonal d).IsHermitian ↔ ∀ (i : n), IsSelfAdjoint (d i)

A diagonal matrix is Hermitian if each diagonal entry is self-adjoint

source
@[simp]
theorem Matrix.isHermitian_diagonal {α : Type u_1} {n : Type u_4} [AddMonoid α] [StarAddMonoid α] [TrivialStar α] [DecidableEq n] (v : n → α) :
(diagonal v).IsHermitian

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

source
@[simp]
theorem Matrix.isHermitian_zero {α : Type u_1} {n : Type u_4} [AddMonoid α] [StarAddMonoid α] :
IsHermitian 0
source
@[simp]
theorem Matrix.IsHermitian.add {α : Type u_1} {n : Type u_4} [AddMonoid α] [StarAddMonoid α] {A B : Matrix n n α} (hA : A.IsHermitian) (hB : B.IsHermitian) :
(A + B).IsHermitian
source
theorem Matrix.isHermitian_add_transpose_self {α : Type u_1} {n : Type u_4} [AddCommMonoid α] [StarAddMonoid α] (A : Matrix n n α) :
(A + A.conjTranspose).IsHermitian
source
theorem Matrix.isHermitian_transpose_add_self {α : Type u_1} {n : Type u_4} [AddCommMonoid α] [StarAddMonoid α] (A : Matrix n n α) :
(A.conjTranspose + A).IsHermitian
source
@[simp]
theorem Matrix.IsHermitian.neg {α : Type u_1} {n : Type u_4} [AddGroup α] [StarAddMonoid α] {A : Matrix n n α} (h : A.IsHermitian) :
(-A).IsHermitian
source
@[simp]
theorem Matrix.IsHermitian.sub {α : Type u_1} {n : Type u_4} [AddGroup α] [StarAddMonoid α] {A B : Matrix n n α} (hA : A.IsHermitian) (hB : B.IsHermitian) :
(A - B).IsHermitian
source
theorem Matrix.isHermitian_mul_conjTranspose_self {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonUnitalSemiring α] [StarRing α] [Fintype n] (A : Matrix m n α) :
(A * A.conjTranspose).IsHermitian

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

source
theorem Matrix.isHermitian_conjTranspose_mul_self {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonUnitalSemiring α] [StarRing α] [Fintype m] (A : Matrix m n α) :
(A.conjTranspose * A).IsHermitian

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

source
@[deprecated Matrix.isHermitian_conjTranspose_mul_self (since := "2025-11-10")]
theorem Matrix.isHermitian_transpose_mul_self {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonUnitalSemiring α] [StarRing α] [Fintype m] (A : Matrix m n α) :
(A.conjTranspose * A).IsHermitian

Alias of `Matrix.isHermitian_conjTranspose_mul_self`.

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

source
theorem Matrix.isHermitian_conjTranspose_mul_mul {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonUnitalSemiring α] [StarRing α] [Fintype m] {A : Matrix m m α} (B : Matrix m n α) (hA : A.IsHermitian) :
(B.conjTranspose * A * B).IsHermitian

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

source
theorem Matrix.isHermitian_mul_mul_conjTranspose {α : Type u_1} {m : Type u_3} {n : Type u_4} [NonUnitalSemiring α] [StarRing α] [Fintype m] {A : Matrix m m α} (B : Matrix n m α) (hA : A.IsHermitian) :
(B * A * B.conjTranspose).IsHermitian

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

source
theorem Matrix.IsHermitian.commute_iff {α : Type u_1} {n : Type u_4} [NonUnitalSemiring α] [StarRing α] [Fintype n] {A B : Matrix n n α} (hA : A.IsHermitian) (hB : B.IsHermitian) :
Commute A B ↔ (A * B).IsHermitian
source
@[deprecated Matrix.IsHermitian.commute_iff (since := "13-08-2025")]
theorem Matrix.commute_iff {α : Type u_1} {n : Type u_4} [NonUnitalSemiring α] [StarRing α] [Fintype n] {A B : Matrix n n α} (hA : A.IsHermitian) (hB : B.IsHermitian) :
Commute A B ↔ (A * B).IsHermitian

Alias of `Matrix.IsHermitian.commute_iff`.

source
@[simp]
theorem Matrix.isHermitian_one {α : Type u_1} {n : Type u_4} [Semiring α] [StarRing α] [DecidableEq n] :
IsHermitian 1

Note this is more general for matrices than `isSelfAdjoint_one` as it does not require `Fintype n`, which is necessary for `Monoid (Matrix n n R)`.

source
@[simp]
theorem Matrix.isHermitian_natCast {α : Type u_1} {n : Type u_4} [Semiring α] [StarRing α] [DecidableEq n] (d : ℕ) :
(↑d).IsHermitian
source
theorem Matrix.IsHermitian.pow {α : Type u_1} {n : Type u_4} [Semiring α] [StarRing α] [Fintype n] [DecidableEq n] {A : Matrix n n α} (h : A.IsHermitian) (k : ℕ) :
(A ^ k).IsHermitian
source
@[simp]
theorem Matrix.isHermitian_intCast {α : Type u_1} {n : Type u_4} [Ring α] [StarRing α] [DecidableEq n] (d : ℤ) :
(↑d).IsHermitian
source
theorem Matrix.IsHermitian.inv {α : Type u_1} {m : Type u_3} [CommRing α] [StarRing α] [Fintype m] [DecidableEq m] {A : Matrix m m α} (hA : A.IsHermitian) :
A⁻¹.IsHermitian
source
@[simp]
theorem Matrix.isHermitian_inv {α : Type u_1} {m : Type u_3} [CommRing α] [StarRing α] [Fintype m] [DecidableEq m] (A : Matrix m m α) [Invertible A] :
A⁻¹.IsHermitian ↔ A.IsHermitian
source
theorem Matrix.IsHermitian.adjugate {α : Type u_1} {m : Type u_3} [CommRing α] [StarRing α] [Fintype m] [DecidableEq m] {A : Matrix m m α} (hA : A.IsHermitian) :
A.adjugate.IsHermitian
source
theorem Matrix.IsHermitian.zpow {α : Type u_1} {m : Type u_3} [CommRing α] [StarRing α] [Fintype m] [DecidableEq m] {A : Matrix m m α} (h : A.IsHermitian) (k : ℤ) :
(A ^ k).IsHermitian

Note that `IsSelfAdjoint.zpow` does not apply to matrices as they are not a division ring.

source
def Matrix.«term_⊕ᵥ_» :
Lean.TrailingParserDescr

Notation for `Sum.elim`, scoped within the `Matrix` namespace.

Equations

- Matrix.«term_⊕ᵥ_» = Lean.ParserDescr.trailingNode `Matrix.«term_⊕ᵥ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕ᵥ ") (Lean.ParserDescr.cat `term 66))

Instances For

source
theorem Matrix.schur_complement_eq₁₁ {α : Type u_1} {m : Type u_3} {n : Type u_4} [CommRing α] [StarRing α] [Fintype m] [DecidableEq m] [Fintype n] {A : Matrix m m α} (B : Matrix m n α) (D : Matrix n n α) (x : m → α) (y : n → α) [Invertible A] (hA : A.IsHermitian) :
vecMul (star (Sum.elim x y)) (fromBlocks A B B.conjTranspose D) ⬝ᵥ Sum.elim x y = vecMul (star (x + (A⁻¹ * B).mulVec y)) A ⬝ᵥ (x + (A⁻¹ * B).mulVec y) + vecMul (star y) (D - B.conjTranspose * A⁻¹ * B) ⬝ᵥ y
source
theorem Matrix.schur_complement_eq₂₂ {α : Type u_1} {m : Type u_3} {n : Type u_4} [CommRing α] [StarRing α] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m m α) (B : Matrix m n α) {D : Matrix n n α} (x : m → α) (y : n → α) [Invertible D] (hD : D.IsHermitian) :
vecMul (star (Sum.elim x y)) (fromBlocks A B B.conjTranspose D) ⬝ᵥ Sum.elim x y = vecMul (star ((D⁻¹ * B.conjTranspose).mulVec x + y)) D ⬝ᵥ ((D⁻¹ * B.conjTranspose).mulVec x + y) + vecMul (star x) (A - B * D⁻¹ * B.conjTranspose) ⬝ᵥ x
source
theorem Matrix.IsHermitian.fromBlocks₁₁ {α : Type u_1} {m : Type u_3} {n : Type u_4} [CommRing α] [StarRing α] [Fintype m] [DecidableEq m] {A : Matrix m m α} (B : Matrix m n α) (D : Matrix n n α) (hA : A.IsHermitian) :
(Matrix.fromBlocks A B B.conjTranspose D).IsHermitian ↔ (D - B.conjTranspose * A⁻¹ * B).IsHermitian
source
theorem Matrix.IsHermitian.fromBlocks₂₂ {α : Type u_1} {m : Type u_3} {n : Type u_4} [CommRing α] [StarRing α] [Fintype n] [DecidableEq n] (A : Matrix m m α) (B : Matrix m n α) {D : Matrix n n α} (hD : D.IsHermitian) :
(Matrix.fromBlocks A B B.conjTranspose D).IsHermitian ↔ (A - B * D⁻¹ * B.conjTranspose).IsHermitian
source
theorem Matrix.IsHermitian.coe_re_apply_self {α : Type u_1} {n : Type u_4} [RCLike α] {A : Matrix n n α} (h : A.IsHermitian) (i : n) :
↑(RCLike.re (A i i)) = A i i

The diagonal elements of a complex Hermitian matrix are real.

source
theorem Matrix.IsHermitian.coe_re_diag {α : Type u_1} {n : Type u_4} [RCLike α] {A : Matrix n n α} (h : A.IsHermitian) :
(fun (i : n) => ↑(RCLike.re (A.diag i))) = A.diag

The diagonal elements of a complex Hermitian matrix are real.

source
theorem Matrix.isHermitian_iff_isSymmetric {α : Type u_1} {n : Type u_4} [RCLike α] [Fintype n] [DecidableEq n] {A : Matrix n n α} :
A.IsHermitian ↔ (toEuclideanLin A).IsSymmetric

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

source
theorem Matrix.IsHermitian.im_star_dotProduct_mulVec_self {α : Type u_1} {n : Type u_4} [RCLike α] [Fintype n] {A : Matrix n n α} (hA : A.IsHermitian) (x : n → α) :
RCLike.im (star x ⬝ᵥ A.mulVec x) = 0