TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

Smith normal form is unique through the gcds of its minors

Statement

Smith normal form is unique and its entries are recovered from successive determinantal divisors. If a matrix has nonzero Smith entries $d_{1} ∣ \dots ∣ d_{r}$ , then, up to associates,

$Δ_{k} = d_{1} \dots d_{k} (0 \leq k \leq r), Δ_{k} = 0 (k > r),$

and $d_{k}$ is the successive quotient $Δ_{k} / Δ_{k - 1}$ .

Facts & Assumptions

Given: Determinantal ideals and divisors from Determinantal divisors from the minors of a matrix over a PID, including $D_{0} = R$ ; determinant multilinearity and alternation (The determinant is the unique normalized alternating multilinear function on the columns).

[L1]

Every rectangular matrix over a PID is equivalent to a Smith diagonal matrix (Every matrix over a PID has a Smith normal form).

Proof

technique · direct

1.1

Every $k$ -minor of $P A$ is an $R$ -linear combination of $k$ -minors of $A$ by determinant multilinearity, so $D_{k} (P A) \subseteq D_{k} (A)$ ; applying the same argument to $P^{- 1}$ gives equality. Right multiplication is identical. Thus equivalent matrices have the same determinantal ideals.

givenalgebra

1.2

For a Smith diagonal matrix with $d_{1} ∣ \dots ∣ d_{r}$ , every nonzero $k$ -minor is a product of $k$ diagonal entries and is divisible by $d_{1} \dots d_{k}$ , while the leading $k$ -minor equals that product. Hence $Δ_{k}$ is associate to $d_{1} \dots d_{k}$ for $k \leq r$ and is $0$ for $k > r$ .

L1algebra

2.1

Step 1.1 makes the $Δ_{k}$ invariants of equivalence. Step 1.2 recovers $r$ as the last nonzero index and recovers each $d_{k}$ up to a unit from successive products, proving uniqueness. It includes $k = 0$ , zero matrices, one-by-one matrices, and all rectangular ranks.

step 1.1step 1.2∎

Depends on

Used by

Smith normal form of an explicit three-by-three integer matrix Example

Dependency tree · two levels

13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

M. Brussel, Finitely Generated Modules over a PID, Theorem 2.1.6 (standard reference, not scraped)
A. Apisa, Wisconsin Math 542, Theorem 27 (standard reference, not scraped)