CorollaryStatement: 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.

The index of a full-rank subgroup of $Z^{n}$ is the absolute determinant of a generating matrix

Statement

Let $n \geq 1$ .

Let $A \in M_{n} (Z)$ and let $L = A Z^{n} \subseteq Z^{n}$ be the subgroup generated by the columns of $A$ . If $\det A \neq 0$ , then the quotient group $Z^{n} / L$ is finite of order $∣ \det A ∣$ ; if $\det A = 0$ , then $Z^{n} / L$ is infinite.
Every subgroup $L \subseteq Z^{n}$ is $A Z^{n}$ for some $A \in M_{n} (Z)$ .

So a subgroup of $Z^{n}$ has finite index exactly when it is generated by the columns of a square integer matrix of nonzero determinant, and its index is then the absolute determinant of every such matrix.

Facts & Assumptions

Given: A natural number $n \geq 1$ , and for clause 1 a matrix $A \in M_{n} (Z)$ with $L = A Z^{n}$ .

[F1]

Abelian groups and $Z$ -modules have the same objects and morphisms, so a subgroup of $Z^{n}$ is a $Z$ -submodule and the quotient group is the quotient module (Abelian groups and $Z$ -modules have the same objects and morphisms). The ring $Z$ is a commutative ring with identity in which a product of nonzero elements is nonzero, so it is an integral domain, and every subgroup of $(Z, +)$ is cyclic, so every ideal of $Z$ is principal: $Z$ is a principal ideal domain (The integers form a commutative ring, The integers have no zero divisors; multiplicative cancellation, Every subgroup of $(Z, +)$ is $⟨ n ⟩ = n Z$ for exactly one natural number $n$ , Principal ideal domain).

[F2]

For every $A \in M_{m \times n} (R)$ over a PID there are invertible $P, Q$ with $P A Q = diag (d_{1}, \dots, d_{r}, 0, \dots, 0)$ and $d_{1} ∣ \dots ∣ d_{r}$ , every $d_{i} \neq 0$ ; equivalence means $B = P A Q$ with $P \in {GL}_{m} (R)$ and $Q \in {GL}_{n} (R)$ (Every matrix over a PID has a Smith normal form, Matrix equivalence and Smith normal form over a PID).

[F3]

Over a commutative ring $\det (A B) = \det (A) \det (B)$ , a square matrix is invertible exactly when its determinant is a unit, the determinant of a triangular matrix is the product of its diagonal entries, and the units of $Z$ are $1$ and $- 1$ (For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ , A positive-sized square matrix over a commutative ring is invertible if and only if its determinant is a unit, The determinant of a triangular matrix is the product of its diagonal entries, $(Z, \cdot, 1)$ is a commutative monoid whose group of units is ${1, - 1}$ ; equivalently $u ∣ 1$ holds exactly for $u = 1$ and $u = - 1$ ).

[F4]

For every module homomorphism $f : M \to N$ there is an isomorphism $M / \ker f ≅ im f$ (First isomorphism theorem for modules: $M / \ker f ≅ im f$ ).

[F5]

For a submodule of a free module of finite rank $n$ over a PID there is a basis $e_{1}, \dots, e_{n}$ of the ambient module and nonzero elements $a_{1} ∣ \dots ∣ a_{r}$ with $r \leq n$ such that $a_{1} e_{1}, \dots, a_{r} e_{r}$ is a basis of the submodule (Simultaneous bases for a submodule of a finite free module over a PID).

Proof

technique · direct

1.1

By [F1] the quotient $Z^{n} / L$ is a quotient of $Z$ -modules, and by [F2] applied over the PID $Z$ there are $P, Q \in {GL}_{n} (Z)$ with $P A Q = D = diag (d_{1}, \dots, d_{r}, 0, \dots, 0)$ , every $d_{i} \neq 0$ .

givenF1F2

1.2

By [F3], $\det P$ and $\det Q$ are units of $Z$ , hence $\pm 1$ , so $∣ \det D ∣ = ∣ \det P ∣ ∣ \det A ∣ ∣ \det Q ∣ = ∣ \det A ∣$ ; and $D$ is diagonal, so $\det D = d_{1} \dots d_{r} \cdot 0^{n - r}$ , which is $d_{1} \dots d_{n}$ when $r = n$ and $0$ when $r < n$ .

givenF3algebra

2.1

Since $Q$ is invertible over $Z$ , $Q Z^{n} = Z^{n}$ , so $A Z^{n} = A Q Z^{n} = P^{- 1} D Z^{n}$ . The map $x \mapsto P x$ is an automorphism of $Z^{n}$ carrying $L = P^{- 1} D Z^{n}$ onto $D Z^{n}$ , so it induces an isomorphism $Z^{n} / L ≅ Z^{n} / D Z^{n}$ .

step 1.1algebra

3.1

Write $d_{i} = 0$ for $r < i \leq n$ , and let $π : Z^{n} \to ⨁_{i = 1}^{n} Z / d_{i} Z$ send $x$ to the tuple of residues $x_{i} + d_{i} Z$ , a surjective homomorphism whose kernel is $D Z^{n}$ . By [F4], $Z^{n} / D Z^{n} ≅ ⨁_{i = 1}^{n} Z / d_{i} Z$ , and with step 2.1 this group is isomorphic to $Z^{n} / L$ .

step 2.1F4algebra

4.1

If $\det A \neq 0$ then $\det D \neq 0$ by step 1.2, so $r = n$ and every $d_{i}$ is nonzero; each $Z / d_{i} Z$ is then finite of order $∣ d_{i} ∣$ , so by step 3.1 the quotient $Z^{n} / L$ is finite of order $∣ d_{1} \dots d_{n} ∣ = ∣ \det D ∣ = ∣ \det A ∣$ .

step 1.2step 3.1algebra

4.2

If $\det A = 0$ then $\det D = 0$ by step 1.2, so $r < n$ and $d_{n} = 0$ ; the summand $Z / d_{n} Z = Z$ is infinite, so by step 3.1 the quotient $Z^{n} / L$ is infinite. This proves clause 1.

step 1.2step 3.1algebra

5.1

For clause 2, let $L$ be any subgroup of $Z^{n}$ . By [F1] it is a $Z$ -submodule of the free module $Z^{n}$ of rank $n$ over the PID $Z$ , so [F5] gives a basis $e_{1}, \dots, e_{n}$ of $Z^{n}$ and nonzero $a_{1} ∣ \dots ∣ a_{r}$ , $r \leq n$ , with $a_{1} e_{1}, \dots, a_{r} e_{r}$ a basis of $L$ . Let $A$ be the matrix whose first $r$ columns are $a_{1} e_{1}, \dots, a_{r} e_{r}$ and whose remaining $n - r$ columns are zero; its entries are integers because the $e_{i}$ and the $a_{i}$ are. Then $A Z^{n}$ is the set of integer combinations of those columns, which is exactly $L$ , so clause 2 holds; combining it with clause 1 gives the final sentence of the Statement.

givenF1F5step 4.1step 4.2construct∎

Remark

The corollary is what makes the determinant a counting invariant: clause 2 says every subgroup of $Z^{n}$ is a column lattice, and for $A$ with nonzero determinant the columns of $A$ generate a subgroup of $Z^{n}$ of index exactly $∣ \det A ∣$ , and the Smith invariant factors $d_{1} ∣ \dots ∣ d_{n}$ refine that single number into the isomorphism type $⨁_{i} Z / d_{i} Z$ of the quotient. Nothing here needs a Euclidean volume: the count comes from the invariant factors, and the determinant enters only because it is unchanged up to sign by multiplication with matrices invertible over $Z$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

77 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 4.2.1 (standard reference, not scraped)

The index of a full-rank subgroup of ZnZn is the absolute determinant of a generating matrix