CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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.

For every fixed finite size at least one, the determinant of a real square matrix is a polynomial in its matrix entries

Statement

For each fixed $n\ge1$ , the function $\det:M_n(\mathbb R)\to\mathbb R$ is evaluation of the polynomial $P_n:=\sum_{\sigma\in S_n}\operatorname{sgn}(\sigma)\prod_{i<n}x_{\sigma(i),i}$ in the $n^2$ commuting variables $x_{ri}$ .

Facts & Assumptions

Given: A fixed natural $n\ge1$ and commuting indeterminates $x_{ri}$ for $r,i<n$ .

[L1]

The determinant is the finite Leibniz sum $\sum_{\sigma}\operatorname{sgn}(\sigma)\prod_i a_{\sigma(i),i}$ (For $n\ge1$ , the determinant over a commutative ring by the Leibniz formula, and $|\det A|$ for a real matrix).

[L2]

Iteration constructs a polynomial ring in any finite list of commuting indeterminates over a commutative ring (Polynomial rings in finitely many commuting indeterminates by iteration).

[L3]

The real numbers form a field (The reals form a field).

[L4]

Every field is a commutative ring with the same operations (Every field is a commutative ring with $1 \ne 0$ ; it is an integral domain, and it is a commutative division ring).

[L5]

Evaluation at a ring element is a unital ring homomorphism, so it respects finite sums and products (Universal property of $R[x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism).

Proof

technique · direct

1.1

By [L2]–[L4], the displayed finite sum of signed monomials is an element $P_n$ of the real polynomial ring in the $n^2$ variables $x_{ri}$ .

L2L3L4

2.1

Iterate [L5] through the finite list of variables, sending each $x_{ri}$ to $a_{ri}$ . The resulting homomorphism sends each monomial to $\prod_{i<n}a_{\sigma(i),i}$ and therefore sends $P_n$ to the Leibniz sum $\det(A)$ from [L1].

step 1.1L1L2L5algebra

3.1

Hence determinant is the polynomial function given by this explicit finite sum of finite products in the matrix entries.

step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 71 results over 14 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

P. Massot, Structures algébriques fondamentales, §6.4 (standard reference, not scraped)