Determinant Multiplicativity

Statement

For any two $n \times n$ matrices $A$ and $B$ over a commutative ring $R$:

Equivalently, $\det : (M_n(R), \cdot) \to (R, \cdot)$ is a monoid homomorphism — and a group homomorphism when restricted to $GL_n(R)$.

Visualization

Take the $2 \times 2$ matrices:

Direct determinants:

Compute $AB$ and its determinant:

Both sides equal $4$, confirming $\det(AB) = \det(A)\,\det(B)$.

Proof Sketch

The standard proof proceeds in two stages. First, note that the result is immediate when $A$ is an elementary row-operation matrix $E$: one checks $\det(E) = \pm 1$ or $c$, and $\det(EB) = \pm \det(B)$ or $c\,\det(B)$ by the row-linearity of $\det$. Second, any invertible $A$ is a product of elementary matrices, so the result follows by induction. When $A$ is singular, $AB$ is singular too ($\operatorname{rank}(AB) \leq \operatorname{rank}(A) < n$), so both sides are $0$.

An elegant alternative: define $f(A) = \det(AB)/\det(B)$ for fixed invertible $B$ and check that $f$ satisfies the defining axioms of the determinant (alternating multilinearity, normalized on $I$), so $f = \det$.

Connections

• Cayley–Hamilton TheoremCayley–Hamilton Theorem$$p_A(A) = 0 \;\text{where}\; p_A(\lambda) = \det(\lambda I - A)$$Every square matrix satisfies its own characteristic polynomialRead more → — the characteristic polynomial $p_A(\lambda) = \det(\lambda I - A)$ uses the determinant; multiplicativity underlies $p_{AB}$ and $p_{BA}$ having the same nonzero eigenvalues.
• Rank–Nullity TheoremRank–Nullity Theorem$$\operatorname{rank}(f) + \operatorname{nullity}(f) = \dim V$$The dimensions of image and kernel of a linear map sum to the domain dimensionRead more → — $\det(A) \neq 0 \iff \operatorname{nullity}(A) = 0 \iff A$ is invertible.
• Cramer's RuleCramer's Rule$$x_i = \frac{\det(A_i)}{\det(A)}$$Explicit determinant formula for the solution of a linear systemRead more → — requires $\det(A) \neq 0$; the proof inverts $A$ using $\det(A)\,A^{-1} = \operatorname{adj}(A)$.
• Spectral TheoremSpectral Theorem$$A = Q \Lambda Q^T \;\text{(real symmetric case)}$$Every real symmetric matrix is orthogonally diagonalizableRead more → — $\det(A) = \prod_i \lambda_i$ follows from the diagonalization $A = Q\Lambda Q^T$ and $\det(Q)\det(Q^T) = 1$.
• Quadratic FormulaQuadratic Formula$$x = \frac{-b \pm \sqrt{b^2 - 4ac}}{2a}$$Solve any quadratic equation using the discriminantRead more → — discriminant $b^2 - 4ac$ is $-\det$ of the associated $2 \times 2$ companion matrix.

/-- Determinant multiplicativity: det(A * B) = det(A) * det(B) for square
    matrices over a commutative ring. Mathlib's proof uses the Leibniz
    formula and permutation group structure. -/
theorem det_multiplicativity {n R : Type*}
    [Fintype n] [DecidableEq n] [CommRing R]
    (A B : Matrix n n R) : (A * B).det = A.det * B.det :=
  Matrix.det_mul A B