Canonical form for nilpotent matrices (Five.III.2)

Open

hefferon_nilpotent_canonical_form

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

canonical-formjordan-formlinear-algebranilpotent

Let $A$ be an $n \times n$ complex matrix that is nilpotent, so $A^m = 0$ for some $m$ . Then $A$ is similar (after reindexing coordinates) to a block-diagonal matrix all of whose blocks are Jordan blocks with eigenvalue zero.

Preamble

import Definitions.Def_hefferon_jordan_form

open Matrix
open HefferonLinAlg

Formal statement

theorem hefferon_nilpotent_canonical_form
    {n : ℕ} (A : Matrix (Fin n) (Fin n) ℂ) (hA : ∃ m : ℕ, A ^ m = 0) :
    ∃ (k : ℕ) (sz : Fin k → ℕ) (e : Fin n ≃ jordanIndex sz)
      (P : Matrix (Fin n) (Fin n) ℂ), IsUnit P.det ∧
        P⁻¹ * A * P = Matrix.reindex e.symm e.symm (jordanMatrix sz fun _ => 0) := by
  sorry

Source

Jim Hefferon, *Linear Algebra*, Saint Michael's College, 2020 printing, Chapter Five, Section III.2, Theorem 2.13, p. 445

View graph