Suppose A is an m-by-n matrix and B is an n-by-m matrix. If S is a subset of {1,...,n} with m elements, we write AS for the m-by-m matrix whose columns are those columns of A that have indices from S. Similarly, we write BS for the m-by-m matrix whose rows are those rows of B that have indices from S. The Cauchy-Binet formula then states
If m = n, i.e. if A and B are square matrices of the same format, then there is only a single admissible set S, and the Cauchy-Binet formula reduces to the ordinary multiplicativity of the determinant. If m = 1 then there are n admissible sets S and the formula reduces to that for the dot product. If m > n, then there is no admissible set S and the determinant det(AB) is zero (see empty sum).
The formula is valid for matrices with entries from any commutative ring. For the proof one writes the columns of AB as linear combinations of the columns of A with coefficients from B, uses the multilinearity of the determinant, and collects the terms that belong to a single det(AS) together by exploiting the anti-symmetry of the determinant. The coefficient of det(AS) is seen to be det(BS) using the Leibniz formula for the determinant. This proof does not use the multiplicativity of the determinant; rather, the proof establishes it.
If A is a real m-by-n matrix, then det(A AT) is equal to the square of the m-dimensional volume of the parallelepiped spanned in Rn by the m rows of A. Binet's formula states that this is equal to the sum of the squares of the volumes that arise if the parallelepiped is orthogonally projected onto the m-dimensional coordinate planes (of which there are C(n,m)). The case m = 1 of this statement talks about the length of a line segment: it is nothing but the Pythagorean theorem.
The Cauchy-Binet formula can be extended in a straight-forward way to a general formula for the minors of the product of two matrices. That formula is given in the article on minors.