uniqueness of the determinant

The deepest fact about determinants is that there is essentially only one. Among all functions that assign a number to an n-by-n matrix, exactly one is alternating, multilinear in the columns, and equal to 1 on the identity matrix. That function is THE determinant. Everything else — the Leibniz sum, cofactor expansion, the product rule — is just this one object wearing different clothes.

Precise statement: let D map n column vectors to a scalar. If D is (i) linear in each column, (ii) zero whenever two columns are equal (alternating), and (iii) D(e_1, ..., e_n) = 1 on the standard basis, then D is uniquely determined and equals det. Sketch: expand each column in the standard basis using multilinearity; the alternating property kills every term with a repeated index, leaving only terms indexed by permutations; condition (iii) fixes their common scale. The surviving sum is exactly the Leibniz formula.

This is the difference between a characterization and a formula. A formula (like Leibniz or Laplace) tells you how to compute; a characterization tells you what the thing IS, so any object satisfying the three properties is forced to coincide with it. That is why you can prove det(AB) = det(A)det(B) without touching a single entry: just check that B -> det(AB) is alternating multilinear, compare its value at the identity, and uniqueness finishes the job.

Caveat: drop the normalization (iii) and you lose uniqueness only up to a scalar — the alternating multilinear functions on n vectors form a one-dimensional space, so any two differ by a constant. Normalizing to 1 on the identity picks the canonical representative. This one-dimensionality is the algebraic shadow of the top exterior power being a line.