Solution (source code)

= Solution

Let $M$ be the <square matrix> whose $j$th column is $A_j$. The <Leibniz formula for determinants> is precisely the stated contraction:
$$
S=\sum_{i_1,\ldots,i_n}\epsilon_{i_1\cdots i_n}M_{i_1,1}\cdots M_{i_n,n}=\det M.
$$
A <square matrix> has zero <determinant> exactly when its columns are <linearly dependent>, proving the required equivalence. One direction also follows directly from <multilinearity> and <antisymmetry of a multilinear map>: replacing one column by a linear combination of the others leaves only terms with repeated columns, each zero. Conversely, nonzero <determinant> gives an <inverse matrix> and hence independent columns.