Eigenvalues and canonical forms

Eigenvalues, eigenspaces and characteristic polynomials of matrices and endomorphisms, and the normal forms they lead to: diagonalization, triangularization, Jordan and Smith normal forms.

• Diagonalization
• Eigenvalues and spectral norm of Hermitian matrices
• Eigenvalues of the products AB and BA
• Generalized eigenvalues of max and min matrices
• Jordan normal form
• Kernels lemma for coprime polynomials
• Newton's identities for traces of matrix powers
• Smith normal form
• Triangularization

TheoremEigenvalues of the inverse matrix#●ready to prove

Let \(M\) be a square matrix over a field \(K\), with rows and columns indexed by a finite type, whose determinant is a unit of \(K\) (so \(M\) is invertible), and let \(\mu \in K\) be nonzero. Then a vector \(x\) is an eigenvector of \(M\) with eigenvalue \(\mu\) (that is, \(x \ne 0\) and \(Mx = \mu x\)) if and only if \(x\) is an eigenvector of \(M^{-1}\) with eigenvalue \(\mu^{-1}\).

theorem_wanted inverse_eigenvalues {n : Type*} [DecidableEq n] [Fintype n]
    {K : Type*} [Field K] (M : Matrix n n K) (hM : IsUnit M.det) {μ : K}
    (hμ : μ ≠ 0) (x : n → K) : Module.End.HasEigenvector (Matrix.toLin' M) μ x ↔
      Module.End.HasEigenvector (Matrix.toLin' M⁻¹) μ⁻¹ x

Sources

• https://en.wikipedia.org/wiki/Eigendecomposition_of_a_matrix.

TheoremSpectral theorem for normal matrices#✓fully proved

Let \(M\) be a complex square matrix whose rows and columns are indexed by a finite set \(n\), and write \(M^*\) for its conjugate transpose. If \(M\) is normal, that is, \(M^* M = M M^*\), then there exist a unitary matrix \(P\) indexed by \(n\) (so \(P^* P = P P^* = I\)) and a family of complex numbers \((d_i)_{i \in n}\) such that \(P^* M P\) is the diagonal matrix with diagonal entries \(d_i\).

public theorem exists_unitary_diagonal_of_isStarNormal
    {n : Type*} [Fintype n] [DecidableEq n]
    {M : Matrix n n ℂ} (hM : IsStarNormal M) :
    ∃ (P : Matrix n n ℂ) (_ : P ∈ Matrix.unitaryGroup n ℂ) (d : n → ℂ),
      star P * M * P = diagonal d

Sources

• AlgebraNotes, Section: The Spectral Theorem, Subsection: The Spectral Theorem, Theorem (Spectral Theorem) (normal-matrix case; the Hermitian cases are Mathlib's Matrix.IsHermitian.spectral_theorem).

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.