Statement of Lagrange's theorem on determinants(elementary question). Apologies for this elementary question; but I was unable to find a reference otherwise.
Let $A, B, C$ be square matrices of the same dimension. Then, 
$$\begin{vmatrix} A & C \\\ 0 & B \end{vmatrix} = |A||B|.$$
The above statement is quite easy to prove using linearity etc properties of the determinant.  However this statement is supposed to be a special case of a general theorem of Lagrange(the existence of which I read about, in Artin's Galois theory book).
So what is this general theorem of Langrange, and could someone please provide a reference? Most stuff is usually in Lang's Algebra, but not this one.
 A: Let $A_{S,T}$ denote the submatrix of $A$ with rows indexed by the elements of $S$ and columns
by the elements of $T$; let $A'_{S,T}$ denote the submatrix of $A$ with rows indexed by the 
elements not in $S$ and columns by the elements not in $T$.  Then we have an expansion
$$
 \det(A) = \sum_T (-1)^{\omega(S,T)} \det(A_{S,T})\det(A'_{S,T})
$$
where $\omega(S,T)=|S|+|T|$ and $S$ is a fixed $k$-subset of the rows of $A$ and $T$ runs over
all $k$-subsets of the columns.
As you can see this makes short work of your identity.  If you can prove the usual row expansion using exterior algebra, you can prove this generalization.  I do not know a reference, but this expansion will be in any of the classical books on determinants
(possibly ascribed to Laplace). It can be used to provide a nice proof of the Pluecker relations, satisfied by the $n\times n$ minors of an $n\times 2n$ matrix.
A: "Special case of a general theorem of Lagrange" doesn't sound well to me: Wikipedia writes that "Lagrange (1773) treated determinants of the second and third order. Lagrange was the first to apply determinants to questions of elimination theory; he proved many special cases of general identities.", so I think your original question is already more general than anything Lagrange has done.
Here are two simple generalizations of your original question:
(1) If
$\left(\begin{array}{cccc}A_{1,1}&A_{1,2}&\dots &A_{1,n} \\\ A_{2,1}&A_{2,2}&\dots &A_{2,n}\\\ \vdots &\vdots &\ddots &\vdots \\\ A_{n,1}&A_{n,2}&\dots &A_{n,n}\end{array}\right)$
is a block matrix with
$A_{i,j}=0$ for every $i < j$, and
$A_{i,i}$ being a square matrix for every $i$,
then its determinant is $\det A_{1,1}\cdot \det A_{2,2}\cdot \dots \cdot \det A_{n,n}$.
The easiest proof (imho) uses the Leibniz formula for determinants, which reduces it to the following combinatorial fact: If a finite set $S$ is the union of some pairwise disjoint sets $S_1$, $S_2$, ..., $S_n$, and $\pi$ is a permutation of the set $S$, then either $\pi\left(S_i\right)=S_i$ for every $i$, or there exist $i < j$ such that $\pi$ maps at least one element of $S_j$ into $S_i$. This is an exercise in induction.
(2) Another generalization: If $\left(U_i\right)_{i\in\mathbb Z}$ is an exact chain complex of finite-dimensional vector spaces, bounded from below and from above (i. e., the vector space $U_i$ is zero for all sufficiently large $i$ and for all sufficiently small $i$), and $\left(f_i\right)_{i\in\mathbb Z}$ is a chain homomorphism from $\left(U_i\right)_{i\in\mathbb Z}$ to $\left(U_i\right)_{i\in\mathbb Z}$, then
$\prod\limits_{i\in\mathbb{Z};\ i\text{ is even}}\det f_i=\prod\limits_{i\in\mathbb{Z};\ i\text{ is odd}}\det f_i$.
