Leibniz formula for determinants

In algebra, the Leibniz formula, named in honor of Gottfried Leibniz, expresses the determinant of a square matrix in terms of permutations of the matrix elements. If "A" is an "n"×"n" matrix, where "a""i","j" is the entry in the "i"th row and "j"th column of "A", the formula is
where sgn is the sign function of permutations in the permutation group "S""n", which returns +1 and −1 for even and odd permutations, respectively.
Another common notation used for the formula is in terms of the Levi-Civita symbol and makes use of the Einstein summation notation, where it becomes
which may be more familiar to physicists.
Directly evaluating the Leibniz formula from the definition requires formula_3 operations in general—that is, a number of operations asymptotically proportional to "n" factorial—because "n"! is the number of order-"n" permutations. This is impractically difficult for large "n". Instead, the determinant can be evaluated in O("n"3) operations by forming the LU decomposition formula_4 (typically via Gaussian elimination or similar methods), in which case formula_5 and the determinants of the triangular matrices "L" and "U" are simply the products of their diagonal entries. (In practical applications of numerical linear algebra, however, explicit computation of the determinant is rarely required.) See, for example, .
Formal statement and proof.
Theorem.
There exists exactly one function
which is alternating multilinear w.r.t. columns and such that formula_7.
Proof.
Uniqueness: Let formula_8 be such a function, and let formula_9 be an formula_10 matrix. Call formula_11 the formula_12-th column of formula_13, i.e. formula_14, so that formula_15
Also, let formula_16 denote the formula_17-th column vector of the identity matrix.
Now one writes each of the formula_11's in terms of the formula_16, i.e.
As formula_8 is multilinear, one has
From alternation it follows that any term with repeated indices is zero. The sum can therefore be restricted to tuples with non-repeating indices, i.e. permutations:
Because F is alternating, the columns formula_24 can be swapped until it becomes the identity. The sign function formula_25 is defined to count the number of swaps necessary and account for the resulting sign change. One finally gets:
as formula_27 is required to be equal to formula_28.
Therefore no function besides the function defined by the Leibniz Formula can be a multilinear alternating function with formula_29. 
Existence: We now show that F, where F is the function defined by the Leibniz formula, has these three properties.
Multilinear:
Alternating:
For any formula_32 let formula_33 be the tuple equal to formula_34 with the formula_35 and formula_36 indices switched.
Thus if formula_38 then formula_39.
Finally, formula_40:
Thus the only alternating multilinear functions with formula_40 are restricted to the function defined by the Leibniz formula, and it in fact also has these three properties. Hence the determinant can be defined as the only function
with these three properties.