### Abstract

A Hermitian matrix is a square complex matrix that is equal to its conjugate transpose. The (finite-dimensional) spectral theorem states that any such matrix can be decomposed into a product of a unitary matrix and a diagonal matrix containing only real elements. We formalize the generalization of this result, which states that any finite set of Hermitian and pairwise commuting matrices can be decomposed as previously, using the same unitary matrix; in other words, they are simultaneously diagonalizable. Sets of pairwise commuting Hermitian matrices are called Complete Sets of Commuting Observables in Quantum Mechanics, where they represent physical quantities that can be simultaneously measured to uniquely distinguish quantum states.

### License

BSD License

### Topics

- Mathematics/Algebra

### Session Commuting_Hermitian

- Commuting_Hermitian_Misc
- Spectral_Theory_Complements
- Commuting_Hermitian

### Depends on

- Quantum projective measurements and the CHSH inequality

### Used by

- The CHSH inequality: Tsirelson’s upper-bound and other results
- Expander Graphs

### Auto-related entries

- Uncertainty Principle

## Cite

×

Commuting_Hermitian-AFP

    @article{Commuting_Hermitian-AFP,
      author  = {Mnacho Echenim},
      title   = {Simultaneous diagonalization of pairwise commuting Hermitian matrices},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Commuting_Hermitian.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Aug 16, 2022 : Isabelle2021-1