Cauchy–Binet Formula

Statement

Let $A$ be an $m \times n$ matrix and $B$ an $n \times m$ matrix over a commutative ring, with $m \le n$. Then

where $A_S$ denotes the $m \times m$ submatrix of $A$ formed by the columns indexed by $S$, and $B^S$ is the $m \times m$ submatrix of $B$ formed by the rows indexed by $S$.

When $m = n$, the only term has $S = [n]$ and we recover the Determinant MultiplicativityDeterminant Multiplicativity$$\det(AB) = \det(A)\,\det(B)$$The determinant of a product equals the product of determinantsRead more → formula $\det(AB) = \det A \cdot \det B$.

Visualization

Take $m = 2$, $n = 3$:

There are $\binom{3}{2} = 3$ index subsets: $S \in \{\{1,2\}, \{1,3\}, \{2,3\}\}$ (1-indexed).

$S$	$A_S$	$\det(A_S)$	$B^S$	$\det(B^S)$	product
$\{1,2\}$	$\begin{pmatrix}1&2\\4&5\end{pmatrix}$	$-3$	$\begin{pmatrix}7&8\\9&10\end{pmatrix}$	$-2$	$6$
$\{1,3\}$	$\begin{pmatrix}1&3\\4&6\end{pmatrix}$	$-6$	$\begin{pmatrix}7&8\\11&12\end{pmatrix}$	$-4$	$24$
$\{2,3\}$	$\begin{pmatrix}2&3\\5&6\end{pmatrix}$	$-3$	$\begin{pmatrix}9&10\\11&12\end{pmatrix}$	$-2$	$6$

Sum: $6 + 24 + 6 = 36$.

Direct computation: $AB = \begin{pmatrix} 58 & 64 \\ 139 & 154 \end{pmatrix}$, $\det(AB) = 58 \cdot 154 - 64 \cdot 139 = 8932 - 8896 = 36$. Confirmed.

Proof Sketch

1. Expand via multilinearity. Write $AB_{ij} = \sum_k A_{ik} B_{kj}$. Expand $\det(AB)$ using multilinearity of the determinant in each row: this gives a sum over functions $f: [m] \to [n]$ of products $\prod_i A_{i,f(i)}$ times an $m \times m$ determinant of columns of $B$ indexed by $f$.
2. Non-injective terms vanish. If $f$ is not injective, two rows of the $B$-submatrix are identical (up to sign), so its determinant is zero.
3. Injective functions = subsets. For injective $f$, grouping by the image set $S = \mathrm{image}(f)$ and summing over permutations of $S$ recovers $\det(A_S)$ from the Leibniz formula. The remaining factor is $\det(B^S)$.
4. Square case. When $m = n$, the only injective $f: [n] \to [n]$ with image $[n]$ are permutations — summing over all of them gives $\det A \cdot \det B$.

Connections

Cauchy–Binet specializes to Determinant MultiplicativityDeterminant Multiplicativity$$\det(AB) = \det(A)\,\det(B)$$The determinant of a product equals the product of determinantsRead more → when $m = n$ and implies Hadamard's InequalityHadamard's Inequality$$|\det A| \le \prod_{j=1}^n \|A_j\|$$The absolute value of a determinant is at most the product of the Euclidean norms of its columns.Read more → (via bounding each minor term). It connects to Rank–Nullity TheoremRank–Nullity Theorem$$\operatorname{rank}(f) + \operatorname{nullity}(f) = \dim V$$The dimensions of image and kernel of a linear map sum to the domain dimensionRead more → through the fact that $\mathrm{rank}(AB) \le \min(\mathrm{rank}(A), \mathrm{rank}(B))$, which follows from counting nonzero terms.

-- Cauchy-Binet for the square case is exactly det_mul.
-- Mathlib: Matrix.det_mul in LinearAlgebra.Matrix.Determinant.Basic
-- For the rectangular case we verify a small numerical instance using decide.
open Matrix in
theorem cauchy_binet_square (n : Type*) [Fintype n] [DecidableEq n]
    (A B : Matrix n n ℚ) :
    det (A * B) = det A * det B :=
  det_mul A B

-- Numerical check: the 2x3 times 3x2 example from the Visualization (over ℤ).
theorem cauchy_binet_check :
    let A : Matrix (Fin 2) (Fin 3) ℤ := !![1, 2, 3; 4, 5, 6]
    let B : Matrix (Fin 3) (Fin 2) ℤ := !![7, 8; 9, 10; 11, 12]
    (A * B).det = 36 := by decide