Operators on finite-dimensional complex spaces have invariant subspaces

Proved

InvariantSubspaceProblem.finite_dimensional_exists_invariant

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-analysisoperator-theory

Let $E$ be a finite-dimensional complex normed space with $\dim_{\mathbb{C}} E\ge 2$ , and let $T\colon E\to E$ be a linear operator. Then $T$ has a non-trivial closed invariant subspace: there is a closed subspace $S$ with $\{0\}\neq S\neq E$ and $T(S)\subseteq S$ .

This is the reason the invariant subspace problem is only posed in infinite dimensions (an eigenvector of $T$ spans such a subspace).

Formalization Note In finite dimensions every subspace is closed and every linear map is bounded, so the statement is the purely algebraic fact.

Preamble

import Definitions.Def_InvariantSubspaceProblem_Defs

Formal statement

namespace InvariantSubspaceProblem

theorem finite_dimensional_exists_invariant (E : Type*) [NormedAddCommGroup E]
    [NormedSpace ℂ E] [FiniteDimensional ℂ E] (hdim : 2 ≤ Module.finrank ℂ E)
    (T : E →L[ℂ] E) : HasNontrivialClosedInvariantSubspace T := by sorry

end InvariantSubspaceProblem

Source

Open Problem Garden, 'Invariant subspace problem' (posted by tchow, 9 Feb 2009), http://www.openproblemgarden.org/op/invariant_subspace_problem (the problem is restricted to infinite-dimensional spaces); Radjavi & Rosenthal, Invariant Subspaces, Springer 1973.

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph