Read-back: HefferonLinAlg.nilpotent_canonical_form

What the declaration literally asserts. Let $K$ be an arbitrary field — the only assumption on $K$ is that it is a field; it is not assumed algebraically closed, infinite, of any particular characteristic, or otherwise constrained — and let $n$ be an arbitrary natural number, including $n = 0$. Let $A$ be an $n \times n$ matrix with entries in $K$, indexed by rows and columns drawn from $\{0, 1, \dots, n-1\}$. The single hypothesis is that $A$ is nilpotent in the sense that some natural-number power of $A$ is the zero matrix: there exists $m \in \mathbb{N}$ with $A^{m} = 0$. (This is the bare existential form; no bound is placed on $m$, in particular it is not required that $m \le n$ or that $A^{n} = 0$. Note that $m = 0$ is formally permitted, in which case the hypothesis reads $I = 0$, which holds only when $n = 0$; for $n \ge 1$ the hypothesis therefore forces some $m \ge 1$ with $A^m = 0$.) The conclusion asserts the existence of a natural number $k$ and a function $sz : \{0, \dots, k-1\} \to \mathbb{N}$ assigning a size $sz_i$ to each index $i$, such that the pair $(sz, \lambda)$ with the constant-zero eigenvalue function $\lambda_i = 0$ for every $i$ is a Jordan form of $A$ in the following unfolded sense. First, every block is nonempty: $sz_i > 0$ for all $i \in \{0, \dots, k-1\}$. Second, writing

for the disjoint union of the block index sets, there exists a bijection $e$ from $\{0,\dots,n-1\}$ onto $S$ (which in particular forces $\sum_{i=0}^{k-1} sz_i = n$, and hence $k \le n$), and there exists an $n \times n$ matrix $P$ over $K$ whose determinant is a unit of $K$ (equivalently, over a field, $\det P \ne 0$, so that $P^{-1}$ is a genuine two-sided inverse rather than the conventional zero-value fallback) satisfying the exact equation

where $J$ is the block-diagonal matrix indexed by $S \times S$ built from Jordan blocks with all eigenvalues equal to $0$, given entrywise by

That is, each diagonal block is the $sz_i \times sz_i$ matrix with zeros on the main diagonal and ones on the subdiagonal (the $1$'s sit one row below the diagonal, at positions where the row index exceeds the column index by exactly one), all off-diagonal blocks are zero, and $\widehat{J}$ is this matrix with its rows and columns relabelled through the bijection $e$. A block of size $1$ is thus the $1 \times 1$ zero matrix.

Quantifier scope and degenerate cases made explicit. $k$, $sz$, $e$ and $P$ are all merely asserted to exist; nothing is claimed about their uniqueness, about the multiset of block sizes being an invariant of $A$, about the blocks being listed in any particular (e.g. weakly decreasing) order, or about any relationship between the block sizes and the nilpotency index $m$. The statement is an implication, not a biconditional: it says nothing about matrices that are not nilpotent, and asserts no converse. The case $n = 0$ is included: there the matrix algebra is the trivial ring, the hypothesis is automatically satisfiable, and $k = 0$ with the empty size function meets the conclusion (the index set $S$ is then empty and $e$ is the empty bijection). The case $k = 0$ is permitted by the conclusion in general, but the bijection requirement makes it usable only when $n = 0$. The relabelling equivalence $e$ is existentially quantified and otherwise unconstrained, so it need not respect any ordering of indices. Finally, the similarity is stated in the direction $P^{-1} A P = \widehat{J}$ (equivalently $A = P \widehat{J} P^{-1}$), with $P$ ranging over matrices of unit determinant.

Form of the artifact. The declaration is stated as a theorem whose proof is left unfilled; only the statement above is asserted.