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

A matrix has rank at least $r$ exactly when it has a nonzero $r$ -rowed minor

Statement

Let $A \in M_{m \times n} (R)$ and let $1 \leq r \leq \min {m, n}$ . Then $rank A \geq r$ if and only if some $r$ -rowed minor of $A$ is nonzero (Submatrices and minors of a rectangular matrix). Equivalently, the rank of $A$ is the largest positive size of a nonzero minor when $A \neq 0$ , and it is $0$ when every entry is zero (The rank of a matrix equals the rank of the linear map $x \mapsto A x$ ).

Facts & Assumptions

Given: A real $m \times n$ matrix $A$ and a natural $r$ with $1 \leq r \leq \min {m, n}$ .

[L1]

The rank of a matrix is the dimension of its column space, because row rank equals column rank (Row space, column space, nullspace, row rank, column rank and matrix rank, Row rank equals column rank, and both equal the number of pivots); a list is independent exactly when only the zero coefficient list has zero linear combination (Linear independence: a finite list $v : n \to V$ is independent when $\sum_{i < n} λ_{i} v_{i} = 0_{V}$ forces every $λ_{i} = 0_{F}$ , and a subset $S \subseteq V$ is independent when every injective finite list into $S$ is independent).

[L2]

A real $r \times r$ matrix has rank $r$ exactly when it is invertible, and it is invertible exactly when its determinant is nonzero (Invertible matrix theorem: invertibility, full pivot rank, RREF $I$ , trivial nullspace and unique solvability are equivalent, A finite square real matrix is invertible if and only if its determinant is nonzero).

Proof

technique · direct

1.1

Suppose first that the $(I, J)$ -minor is nonzero, and write $B = A [I, J]$ for the corresponding $r \times r$ submatrix.

given

1.2

Conversely, suppose $rank A \geq r$ . Choose $r$ independent columns and form the resulting $m \times r$ matrix $C$ . Its column rank and hence its row rank are $r$ , so its rows span $R^{r}$ and contain $r$ independent rows.

givenL1choose

2.1

By [L2], $B$ is invertible. If a linear combination of the $r$ columns of $A$ indexed by $J$ vanishes, restricting that equality to the rows in $I$ gives $B c = 0$ , hence $c = 0$ . Those columns are independent, so $rank A \geq r$ .

step 1.1L1L2

3.1

The $r \times r$ submatrix determined by those columns and rows has rank $r$ , so [L2] makes its determinant nonzero. This is an $r$ -rowed minor of $A$ , proving the converse and the equivalence.

step 1.2L2∎

Depends on

Used by

Dependency tree · two levels

39 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. M. Lee, Introduction to Smooth Manifolds, Theorem 7.13 (standard reference, not scraped)
L. W. Tu, An Introduction to Manifolds, Section 11.1 (standard reference, not scraped)

A matrix has rank at least rr exactly when it has a nonzero rr-rowed minor