LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

$χ_{A} (x)$ is monic of degree $n$ ; for $n \geq 1$ its $x^{n - 1}$ coefficient is $- tr (A)$ and its constant coefficient is $(- 1)^{n} \det (A)$ , while $χ_{0 \times 0} = 1$

Statement

For $A \in M_{n} (F)$ , the polynomial $χ_{A} (x)$ is monic of degree $n$ . If $n \geq 1$ , the coefficient of $x^{n - 1}$ is $- tr (A)$ and the constant coefficient is $(- 1)^{n} \det (A)$ . For $n = 0$ , $χ_{A} (x) = 1$ .

Facts & Assumptions

Given: A matrix $A = (a_{i j}) \in M_{n} (F)$ .

[L1]

For $n \geq 1$ , $χ_{A} (x) = \det (x I_{n} - A)$ ; for $n = 0$ , it is $1$ (For $A \in M_{n} (F)$ , the characteristic polynomial is $χ_{A} (x) = \det (x I_{n} - A)$ when $n \geq 1$ , with $χ_{A} (x) = 1$ for the unique $0 \times 0$ matrix).

[L2]

For $n \geq 1$ , $\det (C) = \sum_{σ \in S_{n}} sgn (σ) \prod_{i < n} c_{σ (i), i}$ (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

[L3]

The trace of $A$ is $\sum_{i < n} a_{i i}$ (The trace $tr (A)$ as the sum of the diagonal entries).

[L4]

The degree of a nonzero polynomial is the largest index of a nonzero coefficient, its leading coefficient is the coefficient at that index, and it is monic when that leading coefficient is $1$ (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

Proof

technique · direct

1.1

If $n = 0$ , [L1] gives $χ_{A} = 1$ , which is monic of degree $0$ ; the additional coefficient assertions are restricted to $n \geq 1$ .

L1L4

1.2

Assume $n \geq 1$ . In [L2] for $x I_{n} - A$ , the identity permutation contributes $\prod_{i < n} (x - a_{i i})$ . Every nonidentity permutation moves at least two indices, so its term contains at most $n - 2$ diagonal factors and has degree at most $n - 2$ .

L1L2algebra

1.3

Evaluating at $x = 0$ gives the constant coefficient $\det (- A) = (- 1)^{n} \det (A)$ directly from [L2].

L1L2algebra

2.1

Hence the coefficient of $x^{n}$ is $1$ , the coefficient of $x^{n - 1}$ comes only from the identity term and is $- \sum_{i < n} a_{i i} = - tr (A)$ , and there are no terms of degree above $n$ . Thus $χ_{A}$ is monic of degree $n$ .

step 1.2L3L4algebra

3.1

Steps 1.1–2.1 establish every asserted dimension and coefficient case.

step 1.1step 2.1step 1.3∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 60 results over 13 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

H. Pinkham, Linear Algebra, §12.1 (standard reference, not scraped)
M. Khovanov, Linear Algebra II notes, §6 (standard reference, not scraped)

χA(x)χA​(x) is monic of degree nn; for n≥1n≥1 its xn−1xn−1 coefficient is −tr⁡(A)−tr(A) and its constant coefficient is (−1)ndet⁡(A)(−1)ndet(A), while χ0×0=1χ0×0​=1