TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-28

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 Binet-Cauchy formula

Statement

Let $A$ be an $m \times n$ matrix and $B$ an $n \times m$ matrix over a commutative ring, where $m \geq 1$ . For an $m$ -element subset $S = {s_{0} < \dots < s_{m - 1}} \subseteq n = {0, \dots, n - 1}$ , let $A [S]$ be the $m \times m$ submatrix of $A$ formed from columns $s_{0}, \dots, s_{m - 1}$ , and let $B [S]$ be the $m \times m$ submatrix of $B$ formed from rows $s_{0}, \dots, s_{m - 1}$ .

If $m > n$ , then $\det (A B) = 0$ . If $m \leq n$ , then

$\det (A B) = \sum_{∣ S ∣ = m} \det (A [S]) \det (B [S]),$

where the sum runs over all $m$ -element subsets $S \subseteq n$ .

Facts & Assumptions

Given: An $m \times n$ matrix $A = (a_{i j})$ and an $n \times m$ matrix $B = (b_{i j})$ over a commutative ring.

[F1]

The determinant is multilinear and alternating in the columns of a square matrix (The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring).

[F2]

For conformable matrices, $(A B)_{i j} = \sum_{r < n} a_{i r} b_{r j}$ (Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose).

[F3]

The determinant is the signed Leibniz sum over the permutations of the column index set (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

Proof

technique · direct

1.1F1F2algebra

Write the columns of $A$ as $a_{0}, \dots, a_{n - 1}$ and the columns of $A B$ as $c_{0}, \dots, c_{m - 1}$ . Then [F2] gives $c_{j} = \sum_{r < n} b_{r j} a_{r}$ for each $j < m$ . By multilinearity of the determinant from [F1], this gives $\det (A B) = \det (c_{0}, \dots, c_{m - 1}) = \sum_{r_{0}, \dots, r_{m - 1} < n} (\prod_{j < m} b_{r_{j}, j}) \det (a_{r_{0}}, \dots, a_{r_{m - 1}})$ .

2.1step 1.1F1

If some index repeats among $r_{0}, \dots, r_{m - 1}$ , then the determinant term vanishes by alternation in [F1]. When $m > n$ , every $m$ -tuple has a repeated index, so all terms vanish and $\det (A B) = 0$ .

3.1step 1.1step 2.1F1F3algebra∎

Assume now that $m \leq n$ . By step 2.1, the sum from step 1.1 may be restricted to tuples whose indices are all distinct. Such tuples are exactly the permutations of the $m$ -element sets $S = {s_{0} < \dots < s_{m - 1}}$ . Grouping together the $m!$ terms attached to one fixed $S$ gives $\sum_{σ \in S_{m}} (\prod_{j < m} b_{s_{σ (j)} j}) \det (a_{s_{σ (0)}}, \dots, a_{s_{σ (m - 1)}}) = \det (A [S]) \det (B [S])$ , because permuting the chosen columns of $A [S]$ contributes the same sign that appears in the Leibniz expansion of $B [S]$ . Summing over all $m$ -element subsets $S$ proves the formula.

Depends on

Used by

Kirchhoff's matrix-tree theorem Theorem

Dependency tree · two levels

19 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

Richard P. Stanley, MIT 18.314 handout, Theorem 1.4 (standard reference, not scraped)