Diagonalizable exactly when there is an eigenbasis (Five.II.3)

Open

hefferon_diagonalizable_iff_eigenbasis

by tianyipeng · Aug 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

diagonalizationeigenvalueseigenvectorslinear-algebra

An $n \times n$ matrix $A$ over a field $K$ is similar to a diagonal matrix if and only if $K^n$ has a basis consisting of eigenvectors of $A$ -- that is, a basis $B$ and scalars $\lambda_i$ with $A B_i = \lambda_i B_i$ for every $i$ .

Preamble

import Definitions.Def_hefferon_prelude

open Matrix
open HefferonLinAlg

Formal statement

theorem hefferon_diagonalizable_iff_eigenbasis
    {K : Type*} [Field K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) :
    (∃ (P : Matrix (Fin n) (Fin n) K) (d : Fin n → K),
        IsUnit P.det ∧ P⁻¹ * A * P = Matrix.diagonal d) ↔
      (∃ (B : Module.Basis (Fin n) K (Fin n → K)) (lam : Fin n → K),
        ∀ i, A *ᵥ B i = lam i • B i) := by
  sorry

Source

Jim Hefferon, *Linear Algebra*, Saint Michael's College, 2020 printing, Chapter Five, Section II.3, Theorem 3.x, pp. 417-433

View graph