Cauchy–Binet formula (source code)

= Cauchy–Binet formula
{c}
{wiki}

For <matrices> $A\in\mathbb R^{r\times m}$ and $B\in\mathbb R^{m\times r}$ with $r\leq m$,
$$
\det(AB)=\sum_{\substack{S\subseteq\{1,\ldots,m\}\\|S|=r}}\det A_{:,S}\det B_{S,:},
$$
where the indices of $S$ are taken in increasing order. To prove it, write the $j$th column of $AB$ as $\sum_q B_{qj}A_{:,q}$ and expand its <determinant> by multilinearity. Terms with a repeated $q$ vanish by alternation. For each remaining index set $S=\{s_1<\cdots<s_r\}$, collect all permutations $q_j=s_{\sigma(j)}$. The factor from $A$ is $\operatorname{sgn}(\sigma)\det A_{:,S}$; the sum of the products $\operatorname{sgn}(\sigma)\prod_j B_{s_{\sigma(j)},j}$ is $\det B_{S,:}$. This proves the formula. Applying it to selected rows and columns proves that a product of compatible <totally nonnegative matrices> is totally nonnegative.