Solution (source code)

= Solution

If a square <matrix> $A$ is an <invertible matrix>, <multiplicativity of the determinant> gives
$$
1=\det I=\det(AA^{-1})=(\det A)(\det A^{-1}),
$$
so $\det A\ne0$.

Conversely, suppose $\det A\ne0$. Use <Gaussian elimination> to reduce $A$ to <row echelon form> $U$. Each <elementary row operation> multiplies the <determinant> by a nonzero factor, so $\det U\ne0$. If this square <matrix> had fewer than $n$ <pivots>, its <row echelon form> would have a zero row and hence zero <determinant>, a contradiction. Therefore it has a <pivot> in every row and column, and further <elementary row operations> reduce it to $I$.

Each <elementary row operation> is multiplication on the left by an <invertible matrix>, its inverse being the reverse operation. Thus $E_k\cdots E_1A=I$ implies $A=E_1^{-1}\cdots E_k^{-1}$, a product of <invertible matrices>. Hence
$$
\boxed{A\text{ is invertible}\iff\det A\ne0.}
$$