### 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

BSD License*Complete Sets of Commuting Observables*in Quantum Mechanics, where they represent physical quantities that can be simultaneously measured to uniquely distinguish quantum states.