(a) Follows from Lemma 5.76 by substituting \(a_1, a_2, \ldots , a_n\) for the indeterminates \(x_1, x_2, \ldots , x_n\). More precisely, the equality

follows from the polynomial identity 13 by applying the evaluation homomorphism \(x_i \mapsto a_i\).

(b) The matrix \(\left( a_j^{n-i} \right)_{1 \leq i \leq n,\; 1 \leq j \leq n}\) is the transpose of the matrix \(\left( a_i^{n-j} \right)_{1 \leq i \leq n,\; 1 \leq j \leq n}\). Thus part (b) follows from part (a) using \(\det (A^T) = \det A\).

(c) The matrix \(\left( a_i^{j-1} \right)\) is obtained from \(\left( a_i^{n-j} \right)\) by reversing the column order. Let \(\tau \in S_n\) send each \(j\) to \(n+1-j\). Then

Since each factor \((a_i - a_j)\) gets negated by \((-1)^\tau \), the result becomes \(\prod _{1 \leq j {\lt} i \leq n} (a_i - a_j)\).

(d) Follows from part (c) using \(\det (A^T) = \det A\).

Set

We must prove that \(f = g\).

By the definition of the determinant,

which is a homogeneous polynomial of degree \(\frac{n(n-1)}{2}\). The monomial \(x_1^{n-1} x_2^{n-2} \cdots x_n^0\) appears with coefficient \(1\) (from the identity permutation \(\sigma = \mathrm{id}\)).

For any \(u {\lt} v\) in \([n]\), setting \(x_u = x_v\) makes two rows of the matrix identical, so \(f\) vanishes. By the root factoring-off theorem (viewing \(f\) as a polynomial in \(x_u\) over \(\mathbb {Z}[x_1, \ldots , \widehat{x_u}, \ldots , x_n]\)), we conclude that \(x_u - x_v\) divides \(f\). Since the ring \(\mathbb {Z}[x_1, \ldots , x_n]\) is a UFD and the linear factors \(x_u - x_v\) are irreducible and mutually non-associate, the product \(g = \prod _{1 \leq i {\lt} j \leq n} (x_i - x_j)\) divides \(f\). Thus \(f = gq\) for some \(q \in \mathbb {Z}[x_1, \ldots , x_n]\).

Since \(\deg f \leq \frac{n(n-1)}{2} = \deg g\), we get \(\deg q \leq 0\), so \(q \in \mathbb {Z}\). Comparing the coefficient of \(x_1^{n-1} x_2^{n-2} \cdots x_n^0\) on both sides gives \(1 = q \cdot 1\), hence \(q = 1\) and \(f = g\).

The formalization relates our matrix convention to Mathlib’s via column reversal, and uses the fact that swapping the order of subtraction in each factor introduces a sign that cancels with the sign from the column permutation.

Let \(C = \left( (x_i + y_j)^{n-1} \right)_{1 \leq i \leq n,\; 1 \leq j \leq n}\). By the binomial formula, for any \(i, j \in [n]\),

Define two \(n \times n\)-matrices

Then \(C = PQ\), so \(\det C = \det P \cdot \det Q\).

From \(Q = \left( y_j^{n-i} \right)\), Theorem 5.75 (b) gives \(\det Q = \prod _{1 \leq i {\lt} j \leq n} (y_i - y_j)\).

From \(P = \left( \binom {n-1}{j-1} x_i^{j-1} \right)\), factoring out the binomial coefficients from each column and applying Theorem 5.75 (c) gives

Hence,

See [ Grinbe15 , Theorem 6.82 ] or [ Ford21 , Lemma 4.7.7 ] or [ Laue15 , 5.8 and 5.8’ ] or [ Strick13 , Proposition B.24 and Proposition B.25 ] or [ Loehr11 , Theorem 9.48 ] .

Part (a) is Mathlib’s Matrix.det_succ_row; part (b) is Matrix.det_succ_column.

(a) Let \(p \in [n]\) satisfy \(p \neq r\). Let \(C\) be the matrix \(A\) with its \(p\)-th row replaced by its \(r\)-th row. Then \(C\) has two equal rows, so \(\det C = 0\). On the other hand, expanding \(\det C\) along the \(p\)-th row (using Theorem 5.79 (a) applied to \(C\)) yields

Comparing gives the claim. Part (b) follows similarly.

The formalization uses the adjugate: \((-1)^{p+q} \det (A_{\sim p, \sim q}) = (\operatorname {adj} A)_{q,p}\), so the sum becomes \(\sum _q A_{r,q} (\operatorname {adj} A)_{q,p} = (A \cdot \operatorname {adj} A)_{r,p} = (\det A) \cdot I_{r,p} = 0\) when \(r \neq p\).

See [ Grinbe15 , Theorem 6.100 ] or [ Ford21 , Lemma 4.7.9 ] or [ Loehr11 , Theorem 9.50 ] or [ Strick13 , Proposition B.28 ] .

To show \(A \cdot (\operatorname {adj} A) = (\det A) \cdot I_n\), it suffices to check that the \((i,j)\)-th entry of \(A \cdot (\operatorname {adj} A)\) equals \(\det A\) when \(i = j\) and equals \(0\) otherwise.

Case \(i = j\): The \((i,i)\) entry is \(\sum _k A_{i,k} (\operatorname {adj} A)_{k,i} = \sum _k (-1)^{i+k} A_{i,k} \det (A_{\sim i, \sim k}) = \det A\) by Laplace expansion along row \(i\) (Theorem 5.79 (a)).

Case \(i \neq j\): The \((i,j)\) entry is \(\sum _k A_{i,k} (\operatorname {adj} A)_{k,j} = \sum _k (-1)^{j+k} A_{i,k} \det (A_{\sim j, \sim k}) = 0\) by Proposition 5.80 (a) (using row \(i\) entries with row \(j\) cofactors).

Similarly, \((\operatorname {adj} A) \cdot A = (\det A) \cdot I_n\) follows using column versions.

See [ Grinbe15 , Theorem 6.156 ] .

The proof partitions the symmetric group based on how permutations map \(P\) to subsets \(Q\) of the same size. For each such \(Q\), the permutations \(\sigma \) with \(\sigma (P) = Q\) decompose as a bijection \(\tau : P \to Q\) (contributing to \(\det (\operatorname {sub}_P^Q A)\)) and a bijection \(\rho : \widetilde{P} \to \widetilde{Q}\) (contributing to \(\det (\operatorname {sub}_{\widetilde{P}}^{\widetilde{Q}} A)\)). The sign decomposes as \((-1)^\sigma = (-1)^{\operatorname {sum} P + \operatorname {sum} Q} (-1)^\tau (-1)^\rho \).

Part (b) follows from part (a) applied to \(A^T\) using \(\det (A^T) = \det A\).

See [ Grinbe15 , Proposition 6.122 ] or [ Bresso99 , § 3.5, proof of Theorem 3.12 ] or [ Zeilbe98 ] .

The proof uses the adjugate matrix.

The right-hand side equals \((\operatorname {adj} A)_{0,0} \cdot (\operatorname {adj} A)_{n-1,n-1} - (\operatorname {adj} A)_{0,n-1} \cdot (\operatorname {adj} A)_{n-1,0}\), which is the \(2 \times 2\) determinant of the corner submatrix of \(\operatorname {adj} A\).

By Jacobi’s complementary minor theorem for the \(2 \times 2\) case (a special case proved independently), this \(2 \times 2\) determinant of the adjugate equals \(\det A \cdot \det (A')\), giving the left-hand side.

The proof of the special case uses the polynomial ring approach: reduce to the generic matrix over the multivariate polynomial ring, then work in its field of fractions where the matrix is invertible.

The proof uses the polynomial version of the identity (factor hunting).

Step 1: Clear denominators. Multiply both sides by \(\prod _{i,j}(x_i + y_j)\) to obtain the “cleared” polynomial identity:

Step 2: Base cases. For \(n = 0, 1, 2, 3\): verified by direct computation.

Step 3: Factor hunting (\(n \geq 4\)): The determinant on the left is a polynomial in \(x_1, \ldots , x_n, y_1, \ldots , y_n\). Setting \(x_i = x_j\) (for \(i \neq j\)) makes two rows identical, so \((x_i - x_j)\) divides the determinant. Similarly, \((y_i - y_j)\) divides the determinant for \(i \neq j\). Since these linear factors are pairwise coprime irreducibles in the UFD \(\mathbb {Z}[x_1, \ldots , x_n, y_1, \ldots , y_n]\), their product divides the determinant.

Step 4: Degree comparison. Both the determinant and the product have total degree \(n(n-1)\), so the quotient is a constant. Evaluating at a specific point shows the constant is \(1\).

Step 5: Recover the Cauchy formula. Dividing the cleared identity by \(\prod _{i,j}(x_i + y_j)\) yields the Cauchy determinant formula.

The proof uses factor hunting in the polynomial ring. Both sides are polynomials of degree \(n(n-1)\) in the \(x_i\)’s and \(y_j\)’s. The left-hand side vanishes when \(x_u = x_v\) (two rows become identical) and when \(y_u = y_v\) (two columns become proportional). Thus the product \(\prod _{i {\lt} j} (x_i - x_j)(y_i - y_j)\) divides the left-hand side. Degree comparison shows the quotient is a constant, and coefficient comparison shows the constant is \(1\).

See [ Grinbe15 , Theorem 6.126 ] .

The proof combines two identities:

1. Adjugate identity (Lemma 5.94, generalized): The \(2 \times 2\) determinant \((\operatorname {adj} A)_{u,p} (\operatorname {adj} A)_{v,q} - (\operatorname {adj} A)_{u,q} (\operatorname {adj} A)_{v,p}\) equals \((-1)^{p+u+q+v}\) times the product-minus-product expression.

2. Jacobi \(2 \times 2\) identity (Theorem 5.89 for \(|P|=|Q|=2\)): The same \(2 \times 2\) determinant of the adjugate equals \((-1)^{p+u+q+v} \det A \cdot \det (\operatorname {sub}_{[n] \setminus \{ p,q\} }^{[n] \setminus \{ u,v\} } A)\).

Equating the two expressions and canceling \((-1)^{p+u+q+v}\) (which squares to \(1\)) yields the result.

Theorem 5.85 is the particular case \(p = 1\), \(q = n\), \(u = 1\), \(v = n\).

The proof uses the polynomial ring approach (following Prasolov’s Problems and Theorems in Linear Algebra).

Step 1: Reduce to generic matrix. Let \(A'\) be the generic \(n \times n\) matrix with polynomial entries in \(\mathbb {Z}[(x_{i,j})_{1 \leq i,j \leq n}]\). The identity for arbitrary \(A\) over any commutative ring \(R\) follows by applying the evaluation homomorphism \(x_{i,j} \mapsto A_{i,j}\).

Step 2: Work in the field of fractions. Since \(\det (A')\) is a nonzero polynomial, we can embed \(A'\) into the field of fractions \(K\) of the polynomial ring, where \(A'\) becomes invertible.

Step 3: Use \(\operatorname {adj}(A) = \det (A) \cdot A^{-1}\). For invertible \(A\) with \(|P| = |Q| = k\):

Step 4: Complementary minor theorem for inverse. The classical result for invertible \(A\) states:

This is proved using block matrix decomposition.

Step 5: Combine. \(\det (\operatorname {sub}_P^Q(\operatorname {adj} A)) = (\det A)^k \cdot (-1)^{\operatorname {sum} P + \operatorname {sum} Q} \cdot \det (\operatorname {sub}_{\widetilde{Q}}^{\widetilde{P}} A) / \det A = (-1)^{\operatorname {sum} P + \operatorname {sum} Q} (\det A)^{k-1} \det (\operatorname {sub}_{\widetilde{Q}}^{\widetilde{P}} A)\).

Step 6: Pull back. Since the identity holds in \(K\) and the canonical map from the polynomial ring to \(K\) is injective, the identity holds in the polynomial ring, and hence for all matrices \(A\) over any commutative ring.

Theorem 5.88 is the particular case of Theorem 5.89 for \(P = \{ u, v\} \) and \(Q = \{ p, q\} \). Theorem 5.85 is, of course, the particular case of Theorem 5.88 for \(p = 1\), \(q = n\), \(u = 1\), \(v = n\).

Each factor \((v_i - v_j) = -(v_j - v_i)\), and there are \(\binom {m}{2} = m(m-1)/2\) such factors.

For \(i {\lt} j\), we have \(\tau (i) {\gt} \tau (j)\), so every pair is an inversion. The total number of inversions is \(\binom {m}{2}\).

Transpose to a row permutation, apply the row permutation determinant formula, then transpose back.

The polynomial Vandermonde matrix is Mathlib’s Vandermonde matrix with columns permuted by the reversal permutation, so the determinant picks up the sign factor.

Direct computation using \((\operatorname {adj} A)_{i,j} = (-1)^{i+j} \det (A_{\sim j, \sim i})\).

The identity \(\det A \cdot \det (A') = \det (A_{\sim 1,\sim 1}) \cdot \det (A_{\sim 2,\sim 2}) - \det (A_{\sim 1,\sim 2}) \cdot \det (A_{\sim 2,\sim 1})\) reduces to \(\det A \cdot 1 = A_{2,2} \cdot A_{1,1} - A_{1,2} \cdot A_{2,1}\) for a \(2 \times 2\) matrix, which is the definition of \(\det A\).

Direct computation using the explicit \(2 \times 2\) adjugate formula.

Direct expansion of the adjugate entries and the \(3 \times 3\) determinant, followed by algebraic simplification.

The proof shows that the order-preserving injection that skips \(p\) and \(q\), being strictly monotone and having range equal to \(\{ p,q\} ^c\), coincides with the canonical order-preserving enumeration of the complement set, so the two submatrix constructions yield the same matrix.

Follows from \(A^{-1} = (\det A)^{-1} \cdot \operatorname {adj} A\).

Entry-wise, \((\operatorname {adj} A)_{i,j} = \det A \cdot A^{-1}_{i,j}\) for invertible \(A\).

By Lemma 5.101, the adjugate submatrix is \(\det A\) times the inverse submatrix. The determinant of a scalar multiple is \((\det A)^k\) times the original determinant.

By the Schur complement formula, \(\det (M) = \det (D) \cdot \det (A - BD^{-1}C)\). The top-left block of \(M^{-1}\) is \((A - BD^{-1}C)^{-1}\), whose determinant is \(\det (A - BD^{-1}C)^{-1}\). Multiplying gives \(\det (D)\).

Since \(\operatorname {adj}(M) = \det (M) \cdot M^{-1}\) for invertible \(M\), the top-left block of \(\operatorname {adj}(M)\) is \(\det (M) \cdot (M^{-1})_{\text{top-left}}\). Taking the \(k \times k\) determinant yields \((\det M)^k \cdot \det ((M^{-1})_{\text{top-left}})\). By Lemma 5.103, \(\det (M) \cdot \det ((M^{-1})_{\text{top-left}}) = \det D\), so \(\det ((M^{-1})_{\text{top-left}}) = \det D / \det M\), giving the result.

Verify directly that \(A_{\sigma ,\tau } \cdot (A^{-1})_{\tau ,\sigma } = I\) using \((A \cdot A^{-1})_{\sigma (i), \sigma (j)} = \delta _{ij}\).

Rewrite the submatrix as a reindexed matrix and apply the standard determinant reindexing formula.

The proof uses block matrix decomposition. Define sorting equivalences \(\sigma \) and \(\tau \) for \(Q\) and \(P\) respectively (Definition 5.105), which reorder indices so that \(P\)-elements come first. The permuted matrix \(M = A_{\sigma , \tau }\) decomposes into blocks: \(M_{\text{top-left}} = \operatorname {sub}_Q^P(A)\) and \(M_{\text{bottom-right}} = \operatorname {sub}_{Q^c}^{P^c}(A)\). By Lemma 5.106, \((M^{-1})_{\text{top-left}} = \operatorname {sub}_P^Q(A^{-1})\). By Lemma 5.103, \(\det (M) \cdot \det ((M^{-1})_{\text{top-left}}) = \det (M_{\text{bottom-right}})\). The sign factor \((-1)^{\operatorname {sum} P + \operatorname {sum} Q}\) arises from the determinant of the sorting permutation (Lemma 5.107).

By Lemma 5.102,

By Lemma 5.108,

so \(\det (\operatorname {sub}_P^Q(A^{-1})) = (-1)^{\operatorname {sum} P + \operatorname {sum} Q} \det (\operatorname {sub}_{\widetilde{Q}}^{\widetilde{P}} A) / \det A\). Since \(|P| = |Q|\), the exponent becomes \(|Q| - 1\).

By induction on the structure of \(p\) (using the polynomial recursor on constants, sums, and products by a variable). The base case (constants) is trivial. The additive case follows from divisibility of sums. The multiplicative case \(p \cdot x_k\) splits: if \(k = i\), factor as \((p - p|_{x_i = x_j}) \cdot x_i + p|_{x_i = x_j} \cdot (x_i - x_j)\); otherwise, factor as \((p - p|_{x_i = x_j}) \cdot x_k\).

View \(P\) as a univariate polynomial in \(x_0\) over \(R[x_1, \ldots , x_{m+1}]\) (using the canonical isomorphism between \(R[x_0, x_1, \ldots , x_{m+1}]\) and \(R[x_1, \ldots , x_{m+1}][x_0]\)). The hypothesis says that \(x_1\) is a root of this univariate polynomial, so \((X - x_1)\) divides it by the polynomial root theorem. Pulling back through the isomorphism yields \((x_0 - x_1) \mid P\).

Since \(x_i - x_j\) has total degree \(1\) and is primitive (its content is \(1\)), it is irreducible. The degree-\(1\) argument: any nontrivial factorization would require one factor of degree \(0\) (a constant), but a primitive polynomial of positive degree cannot have a non-unit constant factor.

The upper bound follows from \(\deg (f - g) \leq \max (\deg f, \deg g)\) and \(\deg (X_i) = 1\). The lower bound follows from the monomial \(X_i^1\) having nonzero coefficient in \(x_i - x_j\).

The coefficient of the monomial \(x_i^1\) is \(1\), so the GCD of the coefficients is \(1\).

Both are irreducible by Lemma 5.113, and they are non-associate (not equal up to unit multiple) since they involve different variable pairs. Distinct irreducibles in a UFD are coprime.

Substituting \(X_j\) for \(X_i\) makes rows \(i\) and \(j\) identical, so the determinant vanishes. By Lemma 5.112, \((X_i - X_j)\) divides the determinant.

Substituting \(Y_j\) for \(Y_i\) makes columns \(i\) and \(j\) proportional (both become \(\prod _{k \neq i, k \neq j}(X_r + Y_k) \cdot (X_r + Y_j)\)), so the determinant vanishes. The divisibility follows by Lemma 5.112.

The polynomial Cauchy identity (Lemma 5.87) gives \(\det (\prod _{k \neq j}(x_i + y_k)) = \prod _{i {\lt} j}(x_i - x_j)(y_i - y_j)\). The left-hand side equals \(\prod _{i,j}(x_i + y_j) \cdot \det (1/(x_i + y_j))\) since each row of the Cauchy matrix can be multiplied by \(\prod _j (x_i + y_j)\) to clear denominators. Dividing gives the result.