LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

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.

Deleted-row minors of a zero-column-sum matrix agree up to sign

Statement

Let $m \geq 1$ and let $A = (a_{k j})$ be an $(m + 1) \times m$ real matrix of rank $m$ (Row space, column space, nullspace, row rank, column rank and matrix rank) each of whose columns has coordinate sum zero, that is $\sum_{k = 1}^{m + 1} a_{k j} = 0$ for every column index $j$ . For $k = 1, \dots, m + 1$ let $Δ_{k}$ be the determinant (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix) of the $m \times m$ matrix obtained by deleting row $k$ . Then $Δ_{k} \neq 0$ for every $k$ and

$Δ_{k} = (- 1)^{k - 1} Δ_{1} (k = 1, \dots, m + 1);$

in particular all $∣ Δ_{k} ∣$ are equal.

Facts & Assumptions

Given: An integer $m \geq 1$ and an $(m + 1) \times m$ real matrix $A = (a_{k j})$ of rank $m$ whose columns each have coordinate sum zero.

[F1]

Expanding a determinant along its last column, with $M_{k m}$ the determinant of the matrix obtained by deleting row $k$ and the last column and $C_{k m} = (- 1)^{k - 1 + m} M_{k m}$ the corresponding cofactor, gives $\det B = \sum_{k = 1}^{m + 1} b_{k, m + 1} C_{k, m + 1}$ ; a matrix with two equal columns has determinant zero (Laplace expansion computes the determinant along every row and every column over a commutative ring, Deleted-row-and-column minors, cofactors, the cofactor matrix and the adjugate over a commutative ring, A square matrix with a zero column or two equal columns has determinant zero).

[F2]

For a real $m \times (m + 1)$ matrix the rank and the dimension of the kernel satisfy $rank + \dim N = m + 1$ ; transposition does not change the rank (For an $m \times n$ matrix $A$ , $rank (A) + \dim N (A) = n$ , Row rank equals column rank, and both equal the number of pivots, The transpose $A^{T}$ of a matrix).

[F3]

If $A$ is $(m + 1) \times m$ of rank $m$ , then some $m$ -rowed minor of $A$ is nonzero (A matrix has rank at least $r$ exactly when it has a nonzero $r$ -rowed minor).

Proof

Proof technique: build a linear relation among the minors from the equality of two columns of an augmented matrix, then identify the resulting kernel with the all-ones line.

1.1F1given

Fix a column index $j$ and let $B$ be the $(m + 1) \times (m + 1)$ real matrix whose first $m$ columns are the columns of $A$ and whose last column is the $j$ -th column of $A$ ; its entries in the last column are $b_{k, m + 1} = a_{k j}$ . The last column of $B$ equals column $j$ , so $\det B = 0$ , and expanding along the last column as in [F1] gives $\sum_{k = 1}^{m + 1} (- 1)^{k - 1 + m} a_{k j} Δ_{k} = 0$ , because deleting row $k$ and the last column of $B$ leaves exactly the matrix whose determinant is $Δ_{k}$ .

2.1F2step 1.1

Define $c_{k} : = (- 1)^{k - 1 + m} Δ_{k}$ for $k = 1, \dots, m + 1$ . Step 1.1 says $\sum_{k = 1}^{m + 1} a_{k j} c_{k} = 0$ for every column index $j$ , that is $A^{T} c = 0$ for the transpose $A^{T}$ ; and the column-sum hypothesis says $\sum_{k = 1}^{m + 1} a_{k j} \cdot 1 = 0$ for every $j$ , that is $A^{T} 1 = 0$ with $1 = (1, \dots, 1) \neq 0$ .

3.1F2step 2.1

Since $A$ has rank $m$ , its transpose $A^{T}$ has rank $m$ , so by rank-nullity its kernel has dimension $(m + 1) - m = 1$ and is therefore a line. Both $c$ and $1$ lie in that kernel and $1 \neq 0$ , so $c = λ 1$ for some $λ \in R$ .

4.1F3step 3.1∎

By [F3] some $m$ -rowed minor of $A$ is nonzero, and the $m$ -rowed minors of $A$ are exactly the determinants $Δ_{1}, \dots, Δ_{m + 1}$ ; since $c_{k} = \pm Δ_{k}$ , this makes $c \neq 0$ , hence $λ \neq 0$ and $Δ_{k} = (- 1)^{k - 1 + m} λ \neq 0$ for every $k$ . In particular $Δ_{1} = (- 1)^{m} λ$ , so $Δ_{k} = (- 1)^{k - 1 + m} λ = (- 1)^{k - 1} \cdot (- 1)^{m} λ = (- 1)^{k - 1} Δ_{1}$ , which is the claimed sign pattern and nonvanishing.

Depends on

Used by

Regulator of a number field Definition
A unimodular change of generators preserves the regulator determinants Example
The regulator is well defined Theorem

Dependency tree · two levels

35 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

J. S. Milne, Algebraic Number Theory v3.08 (standard reference, not scraped)
Andrew V. Sutherland, MIT 18.785 Lecture 15: Dirichlet's Unit Theorem (Fall 2021) (standard reference, not scraped)