Sylvester Determinant Theorem

Statement

Let $A$ be an $m \times n$ matrix and $B$ an $n \times m$ matrix over a commutative ring $R$. Then

This is sometimes called the Weinstein–Aronszajn identity. A striking consequence: even though $AB$ is $m \times m$ and $BA$ is $n \times n$ (potentially very different sizes), the determinant of the identity-plus product is the same.

Visualization

Take $A = \begin{pmatrix} 1 \\ 2 \end{pmatrix}$ (column vector, $2 \times 1$) and $B = \begin{pmatrix} 3 & 4 \end{pmatrix}$ (row vector, $1 \times 2$).

Left side ($2 \times 2$):

Right side ($1 \times 1$):

Quantity	Value
$I_2 + AB$	$\begin{pmatrix} 4 & 4 \\ 6 & 9 \end{pmatrix}$
$\det(I_2 + AB)$	$12$
$I_1 + BA$	$(12)$
$\det(I_1 + BA)$	$12$

Proof Sketch

1. Block matrix trick. Form the $(m+n)\times(m+n)$ block matrix

2. Two factorisations. Observe:

3. Take determinants. The lower-triangular and upper-triangular factors have determinant $1$, giving $\det M = \det(I_n + BA)$ on the left and $\det M = \det(I_m + AB)$ on the right.

Connections

• Determinant MultiplicativityDeterminant Multiplicativity$$\det(AB) = \det(A)\,\det(B)$$The determinant of a product equals the product of determinantsRead more → — the proof reduces to $\det(M) = \det(L_1)\det(U_1) = \det(U_2)\det(L_2)$ where each triangular factor contributes $1$
• 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 → — when $m \ne n$, the identity $\det(I_m + AB) = \det(I_n + BA)$ shows that the non-zero eigenvalues of $AB$ and $BA$ coincide (both sides factor over these eigenvalues)
• 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 → — a polynomial identity consequence: $\chi_{AB}(t) / t^{m-n} = \chi_{BA}(t)$ (up to sign) follows from Sylvester's theorem applied to $tI - A$

import Mathlib.LinearAlgebra.Matrix.SchurComplement

/-- Sylvester's determinant theorem (Weinstein–Aronszajn identity):
    det(1 + A*B) = det(1 + B*A).
    Mathlib's direct alias is `Matrix.det_one_add_mul_comm`. -/
theorem sylvester_det
    {R : Type*} [CommRing R]
    {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
    (A : Matrix m n R) (B : Matrix n m R) :
    (1 + A * B).det = (1 + B * A).det :=
  Matrix.det_one_add_mul_comm A B