Jordan normal form

jordan_normal_form

Submitter: Kim Morrison.

Notes: Over an algebraically closed field, every endomorphism of Kⁿ has a Jordan-chain basis (every n×n matrix is similar to a block-diagonal Jordan matrix). Trusted helpers (StdSpace, JordanChainBasis) are non-holes. Mathlib has the Jordan–Chevalley–Dunford decomposition but not the Jordan-chain-basis/Jordan normal form. Candidate from §165 of the Knill survey.

Source: C. Jordan (1870). Knill, §165.

Informal solution: Unavailable.

theorem declaration uses `sorry`jordan_normal_form {K : Type*} [Field K] [IsAlgClosed K] (n : ℕ)
    (f : Module.End K (LeanEval.LinearAlgebra.JordanNormalForm.StdSpace K n)) :
    Nonempty (LeanEval.LinearAlgebra.JordanNormalForm.JordanChainBasis f) := byK:Type u_1inst✝¹:Field Kinst✝:IsAlgClosed Kn:ℕf:Module.End K (StdSpace K n)⊢ Nonempty (JordanChainBasis f)
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 10, 2026