01.01.07 · foundations / linear-algebra

Determinant: axiomatic + expansion + properties

shipped3 tiersLean: partial

Anchor (Master): Apostol Calculus Vol. 2 Ch. 3; Axler — Linear Algebra Done Right Ch. 10; Bourbaki — Algèbre Ch. III (multilinear algebra)

Intuition [Beginner]

A determinant assigns one number to a square block of numbers. The number measures how much the block stretches or shrinks area when the columns are read as arrows in the plane, or volume when the columns are read as arrows in space. Stretch by a factor of two and the area doubles, fold the block flat and the area drops to zero.

The sign of the number records orientation. Two columns drawn anticlockwise give a positive answer; swap them and the columns now run clockwise, so the answer flips sign. Three columns in space follow the right-hand rule the same way: a positive determinant says the three column-arrows form a right-handed frame, a negative determinant says left-handed.

A determinant of zero is the test for dependence among the columns. If one column is built out of the others, the block has no area or volume to measure, and the answer drops to zero.

Visual [Beginner]

The left panel shows two column-arrows in the plane, the vectors $(2, 3)$ and $(1, 4)$ . Together they outline a parallelogram. The signed area of that parallelogram, with the orientation set by sweeping from the first column to the second anticlockwise, is the determinant of the two-by-two block with those columns. The number works out to $5$ .

The right panel shows the same two columns with their order swapped. The parallelogram is the same shape, but the orientation now sweeps the other way around: the signed area is $- 5$ . Swapping two columns flips the sign of the determinant.

Worked example [Beginner]

Compute the determinant of the two-by-two block

(2314) .

The rule for a two-by-two block is $a d - b c$ , where $a$ and $d$ are the entries on the main diagonal and $b$ and $c$ the entries on the other diagonal. Multiply the diagonal entries: $2 \times 4 = 8$ . Multiply the off-diagonal entries: $1 \times 3 = 3$ . Subtract: $8 - 3 = 5$ .

Read the same number geometrically. The first column is the arrow $(2, 3)$ , the second column is the arrow $(1, 4)$ . The two arrows are not parallel, so they outline a parallelogram in the plane. The signed area of that parallelogram, oriented by sweeping from the first column to the second anticlockwise, is $5$ .

Now swap the two columns to get the block with columns $(1, 4)$ and $(2, 3)$ . The rule gives $1 \times 3 - 2 \times 4 = - 5$ . The parallelogram is the same shape, but the sweep is reversed, so the signed area picks up a minus sign.

What this tells us: the determinant of a two-by-two block is a single number that measures both how much area the columns enclose and which way the columns sweep. Multiply the diagonals, subtract the off-diagonals, and read the signed area.

Check your understanding [Beginner]

Exercise (easy, multiple choice).

The determinant of the block

(6293)

is which of the following, and why?

A. $0$ , because the second column is half the first column B. $0$ , because the second row is one-third the first row C. $9$ , by the diagonal rule D. $- 9$ , by the diagonal rule

Hint

Either apply the rule $a d - b c$ , or notice a dependence among the columns.

Answer

A. $0$ , because the second column is half the first column.

Feedback-correct: correct; the second column $(9, 3)$ equals $1.5$ times the first column $(6, 2)$ , so the columns are dependent and the parallelogram collapses to a line of zero area. The diagonal rule confirms: $6 \times 3 - 9 \times 2 = 18 - 18 = 0$ . Feedback-wrong: option B reads dependence among rows rather than columns and still gives $0$ , but for the wrong reason in the column-based geometric picture; options C and D miscompute the rule.

Formal definition [Intermediate+]

Let $k$ be a field and let $M_{n} (k)$ denote the set of $n \times n$ matrices with entries in $k$ . The standard data of this unit is a function $det : M_{n} (k) \to k$ that admits three equivalent definitions; each is taken as a starting point in some standard treatment, and the equivalence of the three is the first theorem of the subject.

Axiomatic characterisation. The function $det$ is the unique function $M_{n} (k) \to k$ that satisfies

(D1) multilinearity in the rows: for each row index $i$ , and for any matrices $A$ that differ only in row $i$ , the assignment $row_{i} (A) \mapsto det A$ is $k$ -linear;

(D2) alternation: if two distinct rows of $A$ coincide, then $det A = 0$ (equivalently in characteristic different from $2$ , swapping two rows flips the sign of $det A$ );

(D3) normalisation: $det I_{n} = 1$ , where $I_{n}$ is the $n \times n$ identity matrix.

The same axioms with "row" replaced by "column" yield the same function. This is the modern axiomatic presentation; see ^{[textbooks-extra Calculus Vol.2 - Multi-Variable Calculus and Linear Algebra with Applications (Tom Apostol).pdf]} Ch. 3 §3.1–§3.5 and ^{[Artin, E. — Galois Theory]}.

Leibniz permutation-sum formula. Writing $S_{n}$ for the symmetric group on $n$ symbols and $sgn (σ) \in {+ 1, - 1}$ for the sign of a permutation,

det A = σ \in S_{n} \sum sgn (σ) i = 1 \prod n a_{i, σ (i)} .

The sum contains $n!$ terms, each a signed product of $n$ entries chosen one per row and one per column.

Cofactor / Laplace expansion. Fix a row index $i$ . Write $M_{ij}$ for the $(i, j)$ minor of $A$ , the determinant of the $(n - 1) \times (n - 1)$ matrix obtained by deleting row $i$ and column $j$ from $A$ . The Laplace expansion along row $i$ is

det A = j = 1 \sum n (- 1)^{i + j} a_{ij} M_{ij} .

The same formula with $i$ and $j$ exchanged gives the expansion along column $j$ . The factor $(- 1)^{i + j} M_{ij}$ is the $(i, j)$ cofactor of $A$ , written $C_{ij}$ .

For $n = 1$ , the determinant is the single entry: $det (a) = a$ . For $n = 2$ , all three definitions reduce to $a d - b c$ for $(a c b d)$ . For $n = 3$ , the Leibniz formula yields the standard six-term Sarrus expansion. See ^{[quantum-well md/Mathematical foundations/Algebra/Linear Algebra and Matrix Theory/Determinants.md]} for the matrix-group framing.

Notation. The determinant of $A$ is variously written $det A$ , $∣ A ∣$ , or $det (a_{ij})$ . The terms minor, cofactor, and adjugate (the transpose of the cofactor matrix) belong to the same family of derived data; the adjugate $adj (A)$ satisfies $A \cdot adj (A) = det (A) \cdot I_{n}$ .

Counterexamples to common slips

$det (A + B) \neq = det A + det B$ in general: multilinearity is in each row separately, holding the others fixed, not in the matrix as a whole. The two-by-two example $A = B = I_{2}$ gives $det (2 I_{2}) = 4$ while $det I_{2} + det I_{2} = 2$ .
$det (c A) = c^{n} det A$ , not $c det A$ : multilinearity in each of $n$ rows contributes a factor of $c$ .
A determinant of $0$ does not say the matrix is the zero matrix; it says the columns (equivalently rows) are linearly dependent. The two-by-two matrix $(1111)$ has determinant $0$ with no zero entries.
The cofactor expansion uses the sign $(- 1)^{i + j}$ attached to the minor; the unsigned minor $M_{ij}$ alone does not give the determinant.

Key theorem with proof [Intermediate+]

Theorem (multiplicativity). Let $A, B \in M_{n} (k)$ . Then

det (A B) = det A \cdot det B .

^{[textbooks-extra Calculus Vol.2 - Multi-Variable Calculus and Linear Algebra with Applications (Tom Apostol).pdf]}

Proof. Fix the matrix $B$ and define the function $f : M_{n} (k) \to k$ by $f (A) = det (A B)$ . The plan is to show that $f$ satisfies axioms (D1) and (D2) of the axiomatic characterisation, conclude that $f (A) = c (B) \cdot det A$ for some scalar $c (B)$ depending only on $B$ , and pin down $c (B) = det B$ by evaluating at $A = I_{n}$ .

Multilinearity of $f$ in the rows of $A$ . The $i$ -th row of $A B$ is the linear combination $\sum_{j} a_{ij} \cdot (row j of B)$ . Hence the assignment $row_{i} (A) \mapsto row_{i} (A B)$ is $k$ -linear with the other rows of $A$ held fixed. Composing with the determinant, which is multilinear in the rows of $A B$ by axiom (D1) applied to $det$ , gives that $row_{i} (A) \mapsto det (A B) = f (A)$ is $k$ -linear with the other rows of $A$ held fixed. The same holds for every row index $i$ , so $f$ satisfies (D1).

Alternation of $f$ in the rows of $A$ . If two rows of $A$ coincide, say row $i$ and row $i^{'}$ , then the corresponding rows of $A B$ also coincide, since each is the same linear combination of the rows of $B$ . Hence $det (A B) = 0$ by axiom (D2) applied to $det$ , and so $f (A) = 0$ . The function $f$ satisfies (D2).

Pin down the scalar. Multilinearity (D1) and alternation (D2) together imply that any function $g : M_{n} (k) \to k$ satisfying both is determined by its value on the identity; concretely, expansion of $g (A)$ in the standard basis of rows reduces the value to a sum of values of $g$ on row-permutation matrices, each of which equals $sgn (σ) \cdot g (I_{n})$ by alternation. Apply this to $f$ : there exists a scalar $c (B) \in k$ such that $f (A) = c (B) \cdot det A$ for every $A$ . Evaluate at $A = I_{n}$ :

c (B) = c (B) \cdot det I_{n} = f (I_{n}) = det (I_{n} B) = det B .

So $c (B) = det B$ , and $f (A) = det A \cdot det B$ . Substituting back,

det (A B) = f (A) = det A \cdot det B .

$□$

Corollary (invertibility). A square matrix $A \in M_{n} (k)$ is invertible if and only if $det A \neq = 0$ . When invertible, $det (A^{- 1}) = (det A)^{- 1}$ .

Proof. Suppose $A$ is invertible with inverse $A^{- 1}$ . Apply multiplicativity to the identity $A \cdot A^{- 1} = I_{n}$ :

det A \cdot det (A^{- 1}) = det I_{n} = 1.

The product of two field elements equals $1$ , so neither factor can be $0$ ; in particular $det A \neq = 0$ and $det (A^{- 1}) = (det A)^{- 1}$ .

Conversely, suppose $det A \neq = 0$ . The columns of $A$ , viewed as vectors in $k^{n}$ , are then linearly independent: if a linear dependence $\sum_{j} c_{j} \cdot col_{j} (A) = 0$ held with not all $c_{j}$ zero, then one column could be written in terms of the others, the matrix would have a column equal to a linear combination of the rest, and multilinearity together with alternation would force $det A = 0$ . Linear independence of $n$ vectors in $k^{n}$ is equivalent (by 01.01.05) to the linear map $T_{A} : k^{n} \to k^{n}$ defined by left-multiplication by $A$ being injective; in finite-dimensional spaces, injectivity is equivalent to surjectivity, hence to bijectivity, hence to invertibility of $A$ . $□$

Bridge. Multiplicativity is the load-bearing identity from which essentially every property of the determinant flows, and the axiomatic proof above is the canonical route to it. First synthesis: the determinant is a group homomorphism $det : GL_{n} (k) \to k^{\times}$ from the general linear group to the multiplicative group of the field; the kernel is the special linear group $SL_{n} (k)$ , and the short exact sequence $1 \to SL_{n} (k) \to GL_{n} (k) \to k^{\times} \to 1$ is the structural identity that organises the linear-group strand. Second synthesis: combined with the corollary, multiplicativity reduces solving the linear system $A x = b$ to inverting a single scalar — Cramer's rule expresses $x_{i} = det (A_{i}) / det (A)$ , where $A_{i}$ is $A$ with column $i$ replaced by $b$ , recovering the explicit-formula content of invertibility. Third synthesis: the same multiplicativity yields the change-of-variables Jacobian $∣ det J_{g} ∣$ in multivariable integration; the geometric content is that a $C^{1}$ diffeomorphism scales infinitesimal volume by $∣ det J ∣$ , and the multiplicativity identity becomes the chain rule for that scaling under composition of diffeomorphisms. Fourth synthesis: passing to characteristic-polynomial language, $χ_{A} (t) = det (t I - A)$ packages the eigenvalue spectrum of $A$ as the roots of a degree- $n$ polynomial, with the determinant $det A = (- 1)^{n} χ_{A} (0)$ recording the constant term and the trace $tr A$ recording the next-to-leading coefficient; the determinant-and-trace pair generates all symmetric polynomials in the eigenvalues by the Newton identities, so every coordinate-free invariant of a linear operator is a polynomial in $det$ and $tr$ of its iterates.

Exercises [Intermediate+]

Exercise 3 (medium, symbolic).

Compute the Vandermonde determinant for $n = 3$ with parameters $x_{1}, x_{2}, x_{3}$ :

V (x_{1}, x_{2}, x_{3}) = det 111 x_{1} x_{2} x_{3} x_{1}^{2} x_{2}^{2} x_{3}^{2} .

Show that the answer is $(x_{3} - x_{2}) (x_{3} - x_{1}) (x_{2} - x_{1})$ .

Hint

Subtract row $1$ from rows $2$ and $3$ , then expand along the first column.

Answer

Row operations of the form "subtract a multiple of one row from another" do not change the determinant. Subtract row $1$ from row $2$ and from row $3$ :

V = det 100 x_{1} x_{2} - x_{1} x_{3} - x_{1} x_{1}^{2} x_{2}^{2} - x_{1}^{2} x_{3}^{2} - x_{1}^{2} .

Expand along the first column to get

V = det (x_{2} - x_{1} x_{3} - x_{1} x_{2}^{2} - x_{1}^{2} x_{3}^{2} - x_{1}^{2}) .

Factor $x_{2}^{2} - x_{1}^{2} = (x_{2} - x_{1}) (x_{2} + x_{1})$ and $x_{3}^{2} - x_{1}^{2} = (x_{3} - x_{1}) (x_{3} + x_{1})$ , pull $(x_{2} - x_{1})$ from the first row and $(x_{3} - x_{1})$ from the second row:

V = (x_{2} - x_{1}) (x_{3} - x_{1}) \cdot det (11 x_{2} + x_{1} x_{3} + x_{1}) = (x_{2} - x_{1}) (x_{3} - x_{1}) (x_{3} - x_{2}) .

Reordering gives $(x_{3} - x_{2}) (x_{3} - x_{1}) (x_{2} - x_{1})$ , as required. The general Vandermonde determinant is $\prod_{i < j} (x_{j} - x_{i})$ , by the same induction.

Exercise 6 (medium, proof).

Show that if $A$ is block upper triangular, with square diagonal blocks $A_{1}, \dots, A_{r}$ , then $det A = det A_{1} \cdot det A_{2} \dots det A_{r}$ .

Hint

Reduce to the case $r = 2$ by induction, then expand the Leibniz sum and observe that only permutations preserving the block decomposition contribute.

Answer

Reduce to $r = 2$ by induction on $r$ (the inductive step pairs the last block with the rest). For $r = 2$ , write $A = (A_{1} 0 C A_{2})$ , with $A_{1}$ of size $p \times p$ , $A_{2}$ of size $q \times q$ , and $p + q = n$ . In the Leibniz sum $det A = \sum_{σ} sgn (σ) \prod_{i} a_{i, σ (i)}$ , only permutations $σ$ that send ${1, \dots, p}$ to ${1, \dots, p}$ contribute, because any $σ$ that sends some $i \leq p$ to some $j > p$ would require some $i^{'} > p$ to land in ${1, \dots, p}$ , picking up a zero entry from the lower-left block. The contributing $σ$ split uniquely as $σ_{1} \in S_{p}$ on the top block and $σ_{2} \in S_{q}$ on the bottom block, with $sgn (σ) = sgn (σ_{1}) \cdot sgn (σ_{2})$ . The sum factors:

det A = σ_{1} \in S_{p} \sum sgn (σ_{1}) i = 1 \prod p (A_{1})_{i, σ_{1} (i)} \cdot σ_{2} \in S_{q} \sum sgn (σ_{2}) j = 1 \prod q (A_{2})_{j, σ_{2} (j)} = det A_{1} \cdot det A_{2} .

Exercise 7 (hard, proof).

Prove Cramer's rule: if $A \in M_{n} (k)$ is invertible and $b \in k^{n}$ , then the unique solution $x$ of $A x = b$ satisfies $x_{i} = det (A_{i}) / det (A)$ , where $A_{i}$ is the matrix obtained from $A$ by replacing its $i$ -th column with $b$ .

Hint

Write $b = A x = \sum_{j} x_{j} \cdot col_{j} (A)$ and substitute into the $i$ -th column of $A_{i}$ ; then apply multilinearity and alternation.

Answer

By assumption, $b = A x = \sum_{j = 1}^{n} x_{j} \cdot col_{j} (A)$ . Substitute this into the $i$ -th column of $A_{i}$ :

det A_{i} = det [col_{1} (A), \dots, col_{i - 1} (A), \sum_{j} x_{j} col_{j} (A), col_{i + 1} (A), \dots, col_{n} (A)] .

Multilinearity in the $i$ -th column expands the bracket as $\sum_{j} x_{j} det B_{j}$ , where $B_{j}$ is $A$ with its $i$ -th column replaced by $col_{j} (A)$ . For $j \neq = i$ , the matrix $B_{j}$ has two equal columns (the $j$ -th and the $i$ -th), so $det B_{j} = 0$ by alternation. The only surviving term is $j = i$ , where $B_{i} = A$ and $det B_{i} = det A$ . Hence $det A_{i} = x_{i} \cdot det A$ . Since $A$ is invertible, $det A \neq = 0$ , and $x_{i} = det A_{i} / det A$ .

Lean formalization [Intermediate+]

Mathlib packages the determinant as Matrix.det, the Leibniz formula as Matrix.det_apply, multilinearity and alternation in the rows as Matrix.det_updateRow_* together with Matrix.det_smul_row and Matrix.det_swap_rows, multiplicativity as Matrix.det_mul, and the invertibility-iff-non-vanishing characterisation as Matrix.isUnit_iff_isUnit_det. The companion file Codex.Foundations.LinearAlgebra.Determinant records the statements used above and packages the multiplicativity identity in the Codex namespace.

[object Promise]

This unit is marked lean_status: partial because Mathlib supplies every named ingredient — Matrix.det, the Leibniz formula Matrix.det_apply, the multilinearity / alternation lemmas, multiplicativity Matrix.det_mul, and the invertibility characterisation Matrix.isUnit_iff_isUnit_det — but the unified axiomatic uniqueness theorem, together with the determinant-line-bundle generalisation $det V = Λ^{rank V} V$ beyond Matrix.det, is not packaged as a single named module; the corresponding statement in the companion module is left as a sorry-gated alias.

Advanced results [Master]

Exterior-power realisation. Let $V$ be an $n$ -dimensional $k$ -vector space. The $n$ -th exterior power $Λ^{n} V$ is one-dimensional; fixing an isomorphism $Λ^{n} V ≅ k$ is equivalent to choosing an orientation. A linear endomorphism $A : V \to V$ induces a linear endomorphism $Λ^{n} A : Λ^{n} V \to Λ^{n} V$ , which under the chosen isomorphism is multiplication by a scalar. That scalar is $det A$ . Multilinearity and alternation of $det$ in the rows are the statement that $Λ^{n}$ is a multilinear alternating functor of the rows of $A$ ; normalisation $det I = 1$ is the statement that $Λ^{n} id = id$ . The axiomatic characterisation of the determinant is therefore the universal property of the top exterior power. See ^{[Bourbaki, N. — Algèbre, Ch. III: Algèbre tensorielle, algèbre symétrique, algèbre extérieure]}.

Determinant line bundle. For a finite-rank vector bundle $V \to B$ over a base $B$ (the geometric framing reached in 03.05.02), the assignment $V \mapsto Λ^{rank V} V$ is a line bundle $det V \to B$ , the determinant line bundle. Vector bundle morphisms $T : V \to W$ over $B$ induce line bundle morphisms $det T : det V \to det W$ . The first Chern class $c_{1} (V)$ equals $c_{1} (det V)$ ; the top scalar invariant of $V$ is recorded entirely by its determinant line. Orientation of $V$ corresponds to a global nowhere-vanishing section of $det V$ ; a determinant line bundle without such a section is the obstruction to orientability.

Characteristic polynomial and eigenvalue spectrum. The polynomial $χ_{A} (t) = det (t I - A) \in k [t]$ is monic of degree $n$ , and its roots in an algebraic closure $\overset{ˉ}{k}$ are the eigenvalues of $A$ with algebraic multiplicity. Two scalar invariants are immediate from the coefficients: $χ_{A} (t) = t^{n} - (tr A) \cdot t^{n - 1} + \dots + (- 1)^{n} det A$ , so $tr A$ is the sum of eigenvalues with multiplicity and $det A$ is the product. The Newton identities express every symmetric polynomial in the eigenvalues as a polynomial in the traces $tr A^{k}$ , which by the Cayley-Hamilton identity $χ_{A} (A) = 0$ are polynomials in $tr A$ and $det A$ alone (for $n \leq 2$ ) or more generally in the elementary symmetric polynomials of the eigenvalues.

Computational complexity. Three algorithms compute $det A$ for $A \in M_{n} (k)$ over a field $k$ in which arithmetic is constant-time:

Naïve Leibniz: $O (n \cdot n!)$ field operations from the $n!$ permutations, each contributing $n - 1$ multiplications and one addition.
Cofactor recursion: $T (n) = n \cdot T (n - 1) + O (n)$ , hence $T (n) = O (n!)$ , no improvement asymptotically.
LU decomposition / Gaussian elimination: $O (n^{3})$ field operations, using $det (LU) = det L \cdot det U = \prod_{i} U_{ii}$ for unit-lower-triangular $L$ and upper-triangular $U$ . The decomposition exists when no pivot vanishes, and partial pivoting handles the remaining case.

Strassen-style fast matrix multiplication gives $O (n^{ω})$ matrix multiplication with $ω < 3$ (currently $ω < 2.372$ via Coppersmith-Winograd-Le Gall-Vassilevska Williams refinements). Bunch-Hopcroft (1974) showed that LU decomposition reduces to matrix multiplication in the same complexity, so $det$ is computable in $O (n^{ω})$ field operations. Over $Z$ , bit-complexity bounds are sharper via modular reduction.

Special-form determinants.

Vandermonde determinant. $det (x_{i}^{j - 1})_{i, j = 1}^{n} = \prod_{1 \leq i < j \leq n} (x_{j} - x_{i})$ . The right-hand side vanishes iff two of the $x_{i}$ coincide, recovering the geometric statement that the $n$ vectors $(1, x_{i}, x_{i}^{2}, \dots, x_{i}^{n - 1})$ in $k^{n}$ are linearly dependent iff a coincidence occurs.
Cauchy determinant. $det (1/ (x_{i} - y_{j}))_{i, j = 1}^{n} = \prod_{1 \leq i < j \leq n} (x_{j} - x_{i}) (y_{j} - y_{i}) / \prod_{i, j = 1}^{n} (x_{i} - y_{j})$ , when all $x_{i} - y_{j} \neq = 0$ .
Pfaffian and skew-symmetric matrices. For an antisymmetric matrix $A$ of even size $2 m$ (so $A^{T} = - A$ ), there is a polynomial $Pf (A) \in k [a_{ij}]$ , the Pfaffian, of degree $m$ , satisfying $Pf (A)^{2} = det A$ and $Pf (B^{T} A B) = det (B) \cdot Pf (A)$ . Antisymmetric matrices of odd size have determinant $0$ .
Circulant matrix. A circulant matrix $C$ with first row $(c_{0}, c_{1}, \dots, c_{n - 1})$ has determinant $det C = \prod_{k = 0}^{n - 1} (\sum_{j = 0}^{n - 1} c_{j} ω^{j k})$ , where $ω = e^{2 π i / n}$ is a primitive $n$ -th root of unity. The eigenvalues are the discrete Fourier transform of the first row.

Smith normal form over a PID. Over a principal ideal domain $R$ , every matrix $A \in M_{m, n} (R)$ admits a Smith normal form $A = U D V$ , with $U \in GL_{m} (R)$ , $V \in GL_{n} (R)$ , and $D$ diagonal with diagonal entries $d_{1} ∣ d_{2} ∣ \dots ∣ d_{r}$ , the elementary divisors of $A$ . When $A$ is square and invertible over the fraction field, $det A$ equals the product $d_{1} d_{2} \dots d_{n}$ up to a unit of $R$ . Smith normal form recovers the structure theorem for finitely generated modules over a PID, and the determinant records the product of elementary divisors.

Synthesis. Several threads weave together. First synthesis — the determinant as the universal alternating multilinear functional: axioms (D1)–(D3) characterise $det$ as the unique such object, and this characterisation is the reason every coordinate-free identity it satisfies is structurally inevitable rather than computationally lucky. Second synthesis — the determinant as group homomorphism: $det : GL_{n} (k) \to k^{\times}$ is a surjective group homomorphism with kernel $SL_{n} (k)$ , giving the structural decomposition of the general linear group and the algebraic-K-theoretic identification $K_{1} (k) = k^{\times}$ in the lowest dimension. Third synthesis — the determinant as local volume scale: under a $C^{1}$ change of variables $g$ , infinitesimal volume scales by $∣ det J_{g} ∣$ , the chain rule $J_{f \circ g} = J_{f} \cdot J_{g}$ becomes the multiplicativity identity $det J_{f \circ g} = det J_{f} \cdot det J_{g}$ , and the change-of-variables formula in multivariable integration is the integrated form of that pointwise identity. Fourth synthesis — the determinant as top characteristic class: for a finite-rank vector bundle, the determinant line bundle is the universal target of the first Chern class, and the determinant of a bundle map is the section of the determinant line bundle that records the obstruction to invertibility. Fifth synthesis — the determinant as Pfaffian-squared: for antisymmetric matrices the determinant is a perfect square in the entries, and the square-root Pfaffian is the more refined invariant; this is the prototype for square-root-of-determinant phenomena in spin geometry and in the index theorem for Dirac operators.

Full proof set [Master]

Axiomatic uniqueness theorem. Let $f : M_{n} (k) \to k$ satisfy (D1) multilinearity in rows, (D2) alternation, and (D3) $f (I_{n}) = 1$ . Then $f = det$ . The proof has two parts: first, that $f$ is determined by its values on permutation matrices; second, that those values are the signatures of the corresponding permutations.

Write a matrix $A \in M_{n} (k)$ row by row, $A = (r_{1}, \dots, r_{n})$ with $r_{i} \in k^{n}$ . Expand each $r_{i}$ in the standard basis $e_{1}, \dots, e_{n}$ of $k^{n}$ : $r_{i} = \sum_{j = 1}^{n} a_{ij} e_{j}$ . Multilinearity (D1) in each row separately expands

f (A) = j_{1}, \dots, j_{n} \sum a_{1 j_{1}} a_{2 j_{2}} \dots a_{n j_{n}} \cdot f (e_{j_{1}}, e_{j_{2}}, \dots, e_{j_{n}}),

a sum over all $n^{n}$ index sequences. Alternation (D2) implies $f (e_{j_{1}}, \dots, e_{j_{n}}) = 0$ whenever two of the $j_{i}$ coincide, leaving only the $n!$ sequences that form a permutation; write $j_{i} = σ (i)$ with $σ \in S_{n}$ :

f (A) = σ \in S_{n} \sum (i = 1 \prod n a_{i, σ (i)}) \cdot f (e_{σ (1)}, \dots, e_{σ (n)}) .

It remains to compute $f$ on the permutation matrix $P_{σ} = (e_{σ (1)}, \dots, e_{σ (n)})$ . Alternation implies that swapping two rows of any matrix flips the sign of $f$ : if rows $i$ and $i^{'}$ are swapped, write $A^{'}$ for the swapped matrix and apply multilinearity to the matrix with both rows equal to $r_{i} + r_{i^{'}}$ , which has $f$ -value $0$ by alternation; expanding gives $f (A) + f (A^{'}) = 0$ , so $f (A^{'}) = - f (A)$ . Hence $f (P_{σ}) = sgn (σ) \cdot f (P_{e}) = sgn (σ) \cdot f (I_{n}) = sgn (σ)$ by (D3). Substituting, $f (A) = \sum_{σ} sgn (σ) \prod_{i} a_{i, σ (i)}$ , the Leibniz formula, so $f = det$ on every $A$ . $□$

Equivalence of Leibniz and Laplace. Fix a row index $i$ . Group the terms in the Leibniz sum by the value $σ (i) = j$ :

det A = j = 1 \sum n a_{ij} \cdot (σ : σ (i) = j \sum sgn (σ) i^{'} \neq = i \prod a_{i^{'}, σ (i^{'})}) .

The inner sum runs over permutations $σ$ with $σ (i) = j$ ; restricting $σ$ to ${1, \dots, n} ∖ {i}$ gives a bijection to $S_{n - 1}$ on the index set ${1, \dots, n} ∖ {j}$ . The sign of $σ$ relates to the sign of its restriction by an extra $(- 1)^{i + j}$ , the number of inversions introduced by moving $σ (i) = j$ to its proper position. The inner sum is therefore $(- 1)^{i + j} M_{ij}$ , where $M_{ij}$ is the minor of $A$ obtained by deleting row $i$ and column $j$ . Substituting, $det A = \sum_{j} (- 1)^{i + j} a_{ij} M_{ij}$ , the Laplace expansion along row $i$ . $□$

Adjugate identity. Define the adjugate $adj (A) \in M_{n} (k)$ by $adj (A)_{j i} = (- 1)^{i + j} M_{ij}$ (note the transpose). Then $A \cdot adj (A) = det A \cdot I_{n}$ .

Compute the $(i, k)$ entry of $A \cdot adj (A)$ :

(A \cdot adj (A))_{ik} = j = 1 \sum n a_{ij} \cdot adj (A)_{j k} = j = 1 \sum n a_{ij} \cdot (- 1)^{k + j} M_{k j} .

For $k = i$ , this is the Laplace expansion of $det A$ along row $i$ , giving $det A$ . For $k \neq = i$ , this is the Laplace expansion along row $k$ of the matrix $A^{'}$ obtained from $A$ by replacing row $k$ with row $i$ ; since $A^{'}$ has two equal rows (row $i$ and row $k$ ), alternation gives $det A^{'} = 0$ . Hence the matrix product is $det A \cdot I_{n}$ . When $det A \neq = 0$ , dividing yields $A^{- 1} = det (A)^{- 1} \cdot adj (A)$ , the closed-form inverse. $□$

Cayley-Hamilton via the adjugate. The characteristic polynomial $χ_{A} (t) = det (t I - A)$ is a polynomial of degree $n$ in $t$ with matrix-valued coefficients in the adjugate computation. Working in the polynomial ring $k [t]$ , the adjugate of $t I - A$ has entries that are polynomials of degree at most $n - 1$ in $t$ , and the adjugate identity gives

(t I - A) \cdot adj (t I - A) = χ_{A} (t) \cdot I_{n} .

Write $adj (t I - A) = \sum_{k = 0}^{n - 1} B_{k} t^{k}$ with $B_{k} \in M_{n} (k)$ . Substituting and equating coefficients of like powers of $t$ on both sides gives the system

B_{n - 1} = I_{n}, B_{k - 1} - A \cdot B_{k} = c_{k} \cdot I_{n} for 0 \leq k \leq n - 1, - A \cdot B_{0} = c_{0} \cdot I_{n},

where $χ_{A} (t) = t^{n} + c_{n - 1} t^{n - 1} + \dots + c_{0}$ . Multiply the $k$ -th identity by $A^{k}$ and sum:

k = 0 \sum n - 1 A^{k} (B_{k - 1} - A B_{k}) + A^{n} B_{n - 1} - A^{n} B_{n - 1} = χ_{A} (A) - A^{n} B_{n - 1} + A^{n},

and the telescoping on the left yields $0$ , so $χ_{A} (A) = 0$ as a matrix identity. $□$

Vandermonde determinant by row reduction. Let $V = (x_{i}^{j - 1})_{i, j = 1}^{n}$ . Subtract from each column (starting at the rightmost) $x_{1}$ times the column to its left. Each resulting entry in row $i$ , column $j$ , for $j \geq 2$ , becomes $x_{i}^{j - 1} - x_{1} \cdot x_{i}^{j - 2} = x_{i}^{j - 2} (x_{i} - x_{1})$ . Row $1$ becomes $(1, 0, 0, \dots, 0)$ . Expand along the first row: only the $(1, 1)$ entry contributes, yielding

det V = det (x_{i}^{j - 2} (x_{i} - x_{1}))_{i = 2, \dots, n; j = 2, \dots, n} .

Factor $(x_{i} - x_{1})$ from row $i$ for each $i = 2, \dots, n$ :

det V = i = 2 \prod n (x_{i} - x_{1}) \cdot det (x_{i}^{j - 2})_{i = 2, \dots, n; j = 2, \dots, n} .

The remaining matrix is the Vandermonde of size $n - 1$ on parameters $x_{2}, \dots, x_{n}$ . Induction on $n$ gives $det V = \prod_{1 \leq i < j \leq n} (x_{j} - x_{i})$ . The base case $n = 1$ is $det V = 1$ . $□$

Block-triangular determinant. Recorded in Exercise 6; the proof is the Leibniz-formula factorisation given there. The same argument extends by induction to $r$ blocks.

Pfaffian-squared identity. Stated without proof; one route uses the exterior-algebra realisation of an antisymmetric form $ω \in Λ^{2} V$ on $V$ of dimension $2 m$ . The top exterior power $ω^{m} / m! \in Λ^{2 m} V$ is a scalar multiple of the orientation, and that scalar is $Pf (A)$ when $A$ is the matrix of $ω$ in an orientation-compatible basis; squaring gives $Pf (A)^{2} = det A$ . The full proof is the content of the multilinear-algebra strand and is reached in 01.01.10 pending / 03.01.04. See ^{[Bourbaki, N. — Algèbre, Ch. III: Algèbre tensorielle, algèbre symétrique, algèbre extérieure]}.

Connections [Master]

Linear transformation, kernel, image, rank-nullity 01.01.05 — provides the equivalence between invertibility of a square matrix and full rank of the associated linear map. The determinant test $det A \neq = 0$ records the same condition via the axiomatic alternating property: a dependence among columns forces the determinant to zero, and conversely a non-zero determinant rules out dependence and so forces the kernel to consist of the zero vector alone. The corollary " $A$ invertible iff $det A \neq = 0$ " is therefore the determinant-side dual of the rank-nullity criterion for invertibility.
Eigenvalue, eigenvector, characteristic polynomial 01.01.08 — the characteristic polynomial $χ_{A} (t) = det (t I - A)$ is the determinant of a $t$ -shifted matrix whose roots are the eigenvalues of $A$ . Determinant multiplicativity gives the similarity-invariance $χ_{B^{- 1} A B} (t) = χ_{A} (t)$ , so the eigenvalue spectrum is an intrinsic invariant of the operator class. The two extreme coefficients are the trace $tr A$ and the determinant $det A$ , the sum and product of the eigenvalues respectively.
Differential forms 03.04.02 — the determinant is the coordinate expression of the action of a linear endomorphism on the top exterior power. A top differential form $ω \in Ω^{n} (M)$ on an $n$ -dimensional manifold pulls back along a smooth map $f$ to $f^{*} ω = (det J_{f}) \cdot ω$ in local coordinates, where $J_{f}$ is the Jacobian matrix; this is the differential-forms incarnation of the determinant as local volume scale.
Integration on manifolds 03.04.03 — the change-of-variables formula $\int_{Ω} f = \int_{Ω^{'}} (f \circ g) \cdot ∣ det J_{g} ∣$ for a $C^{1}$ diffeomorphism $g$ rests on the determinant as the scaling factor of $n$ -dimensional Lebesgue measure under a linear transformation. Multiplicativity of $det$ corresponds to the chain rule for Jacobians, and the change-of-variables formula is the integrated pointwise identity.
Vector bundle 03.05.02 — the determinant line bundle $det V = Λ^{rank V} V$ assembles the fibrewise top exterior power into a globally defined line bundle. The first Chern class $c_{1} (V) = c_{1} (det V)$ is the topological invariant carried by the determinant line; the existence of a global trivialisation of $det V$ is equivalent to orientability of $V$ , and a smooth nowhere-vanishing section of $det V$ is an orientation.
Lie group 03.03.01 — the determinant is the structural homomorphism $det : GL_{n} (k) \to k^{\times}$ presenting $SL_{n} (k)$ as its kernel. At the Lie-algebra level this is the trace $tr : gl_{n} (k) \to k$ with kernel $sl_{n} (k)$ , and the linearised relation $det (exp X) = exp (tr X)$ tracks the determinant of one-parameter subgroups of $GL_{n}$ via the trace of the generator.

Historical & philosophical context [Master]

The determinant predates the matrix. Seki Takakazu in Japan (manuscript circulated 1683, Kai Fukudai no Ho) and Gottfried Wilhelm Leibniz in Hanover (letter to L'Hôpital, 28 April 1693) independently developed the determinant as a tool for the elimination of variables from systems of linear equations a century before the matrix entered the literature. Gabriel Cramer's Introduction à l'analyse des lignes courbes algébriques (Geneva, 1750) gave the determinant-quotient formula now bearing his name without using the word determinant. Alexandre-Théophile Vandermonde, in Mémoire sur l'élimination (Histoire de l'Académie Royale des Sciences, 1771), introduced the determinant treated as a function in its own right and computed the special-form determinant that bears his name ^{[Cauchy, A.-L. — Mémoire sur les fonctions qui ne peuvent obtenir que deux valeurs égales et de signes contraires par suite des transpositions opérées entre les variables qu'elles renferment]}.

Augustin-Louis Cauchy's 1815 memoir in the Journal de l'École Polytechnique unified the existing fragments — Vandermonde, Laplace's 1772 expansion in the Recherches sur le calcul intégral, Bézout's resultant — into a single theory of "fonctions symétriques alternées", the alternating multilinear functions of which the determinant is the canonical case. Cauchy proved multiplicativity, gave the Laplace expansion in modern form, and computed many special determinants including the resultant of two polynomials. The vocabulary "determinant" entered the literature with Carl Friedrich Gauss in Disquisitiones Arithmeticae (Leipzig, 1801, §171) in the binary-quadratic-form sense; the modern matrix-determinant sense crystallised through Cauchy and Carl Gustav Jacob Jacobi in the 1820s and 1830s. Arthur Cayley's A memoir on the theory of matrices (Philosophical Transactions of the Royal Society 148, 1858, 17–37) introduced matrix notation and matrix multiplication, retroactively turning the determinant into a function of a single matrix rather than a function of an array of arguments ^{[Cayley, A. — A memoir on the theory of matrices]}.

Karl Weierstrass and Leopold Kronecker, lecturing in Berlin in the 1870s, gave the first axiomatic presentation: the determinant as the unique multilinear alternating normalised function. The presentation was perfected and disseminated by Emil Artin in his Notre Dame lectures of 1942, published as Galois Theory in 1944, where the determinant is developed in an appendix from exactly the three axioms (D1)–(D3) used in this unit ^{[Artin, E. — Galois Theory]}. The Bourbaki Algèbre, Chapter III (Hermann, Paris, 1948), recast the determinant as a special case of the universal property of the top exterior power, embedding it permanently in multilinear algebra ^{[Bourbaki, N. — Algèbre, Ch. III: Algèbre tensorielle, algèbre symétrique, algèbre extérieure]}. The exterior-algebra framing is the modern presentation and the one that generalises cleanly to vector bundles, super-vector-spaces, and the various flavours of non-commutative determinant (Dieudonné determinant, quantum determinant, Berezinian) that arose in the second half of the twentieth century.

Bibliography [Master]

Seki, T., Kai Fukudai no Ho (manuscript circulated 1683, published posthumously in collected works); reproduced in Hayashi, T. (ed.), Takakazu Seki's Collected Works, Osaka, 1974.
Leibniz, G. W., Letter to L'Hôpital, 28 April 1693, in Mathematische Schriften, ed. C. I. Gerhardt, Berlin, 1850–1863, Vol. II, 229.
Cramer, G., Introduction à l'analyse des lignes courbes algébriques, Frères Cramer & Cl. Philibert, Geneva, 1750.
Vandermonde, A.-T., "Mémoire sur l'élimination", Histoire de l'Académie Royale des Sciences, Paris, 1771 (published 1774), 516–532.
Laplace, P.-S., "Recherches sur le calcul intégral et sur le système du monde", Histoire de l'Académie Royale des Sciences, Paris, 1772, 267–376 (cofactor expansion).
Gauss, C. F., Disquisitiones Arithmeticae, Gerh. Fleischer Jun., Leipzig, 1801.
Cauchy, A.-L., "Mémoire sur les fonctions qui ne peuvent obtenir que deux valeurs égales et de signes contraires par suite des transpositions opérées entre les variables qu'elles renferment", Journal de l'École Polytechnique 10 (1815), 29–112.
Jacobi, C. G. J., "De formatione et proprietatibus determinantium", Journal für die reine und angewandte Mathematik 22 (1841), 285–318.
Cayley, A., "A memoir on the theory of matrices", Philosophical Transactions of the Royal Society of London 148 (1858), 17–37.
Bunch, J. R. & Hopcroft, J. E., "Triangular factorization and inversion by fast matrix multiplication", Mathematics of Computation 28 (1974), 231–236.
Artin, E., Galois Theory, Notre Dame Mathematical Lectures No. 2, University of Notre Dame Press, 1942; 2nd ed. 1944.
Bourbaki, N., Algèbre, Chapter III: Algèbre tensorielle, algèbre symétrique, algèbre extérieure, Hermann, Paris, 1948; 2nd ed. 1970.
Apostol, T. M., Calculus, Vol. 2: Multi-Variable Calculus and Linear Algebra with Applications, 2nd ed., John Wiley & Sons, 1969, Ch. 3.
Hoffman, K. & Kunze, R., Linear Algebra, 2nd ed., Prentice-Hall, 1971, Ch. 5.
Axler, S., Linear Algebra Done Right, 3rd ed., Springer, 2015, Ch. 10.

Autonomous production unit. Successor to linear-transformation / rank-nullity; load-bearing for eigenvalues and the characteristic polynomial, for the change-of-variables Jacobian in multivariable calculus, for the top differential form on $R^{n}$ , and for the determinant line bundle in geometry.

Prerequisites

01.01.05

Tier anchors

beginner: 3Blue1Brown — Essence of Linear Algebra Ch. 5–6 (determinant as signed area / volume)
intermediate: Apostol Calculus Vol. 2 Ch. 3 §3.1–§3.10; Hoffman-Kunze — Linear Algebra Ch. 5
master: Apostol Calculus Vol. 2 Ch. 3; Axler — Linear Algebra Done Right Ch. 10; Bourbaki — Algèbre Ch. III (multilinear algebra)

References

quantum-well
md/Mathematical foundations/Algebra/Linear Algebra and Matrix Theory/Determinants.md · determinants entry
textbooks-extra
Calculus Vol.2 - Multi-Variable Calculus and Linear Algebra with Applications (Tom Apostol).pdf · Ch. 3 §3.1–§3.17, determinants axiomatically, Leibniz formula, expansion, multiplicativity, Vandermonde
TODO_REF
Axler, S. — Linear Algebra Done Right (3rd ed.) · Ch. 10, determinants via the axiomatic and exterior-power approaches
TODO_REF
Hoffman, K. & Kunze, R. — Linear Algebra (2nd ed.) · Ch. 5, determinants, multilinear forms, the alternating n-linear function
TODO_REF
Cauchy, A.-L. — Mémoire sur les fonctions qui ne peuvent obtenir que deux valeurs égales et de signes contraires par suite des transpositions opérées entre les variables qu'elles renferment · Journal de l'École Polytechnique 10 (1815), 29–112 — first systematic theory of determinants
TODO_REF
Cayley, A. — A memoir on the theory of matrices · Philosophical Transactions of the Royal Society 148 (1858), 17–37
TODO_REF
Artin, E. — Galois Theory · Notre Dame Mathematical Lectures No. 2, 1942/1971 — axiomatic determinant in Appendix
TODO_REF
Bourbaki, N. — Algèbre, Ch. III: Algèbre tensorielle, algèbre symétrique, algèbre extérieure · Hermann, 1948/1970 — determinant as the top exterior power

Lean module

Codex.Foundations.LinearAlgebra.Determinant

Mathlib gap

Mathlib packages the determinant as Matrix.det together with the Leibniz formula (Matrix.det_apply), multilinearity and alternation in the rows (Matrix.det_updateRow_*, Matrix.det_smul_row, Matrix.det_swap_rows), multiplicativity (Matrix.det_mul), cofactor / Laplace expansion (Matrix.det_succ_row, Matrix.det_succ_column), and the invertibility-iff-non-vanishing characterisation (Matrix.isUnit_iff_isUnit_det). What is not packaged as a single self-contained module is the unified axiomatic uniqueness theorem — the statement that any multilinear-alternating-normalised function on square matrices equals Matrix.det — formulated so that the axiomatic, Leibniz, and Laplace presentations appear as three equally valid starting points with named equivalence lemmas. The determinant-line-bundle generalisation det V = Λ^{rank V} V beyond Matrix.det is also absent; the corresponding statement in the companion module is left as a sorry-gated alias.

Reviewer

TBD

Estimated time

beginner: 20m
intermediate: 45m
master: 80m