The Vandermonde reduction

A square matrix whose entries factor as a column scalar times a power of a column value, M i j = c j * v j ^ (i : ℕ), is a column-rescaled transposed Vandermonde matrix. Its determinant is therefore (∏ j, c j) times the Vandermonde product ∏_{i < j} (v j - v i), and — over a domain, with every c j a unit — it is nonzero exactly when the v j are pairwise distinct.

This is the linear-algebra half of the four ladder lemmas: each of them reduces the last rung det L_{d-1} modulo p to a Vandermonde determinant in the Fermat quotients, and the step that turns "the entries look like c j * v j ^ i" into "the determinant is the Vandermonde product" needs nothing about Fermat quotients whatsoever. It is stated here once, for a general commutative ring.

The d = p case of the paper is the reason the file is more general than the main theorem needs: there the bottom row's exponent is not d - 1 but comes from the exceptional Fermat congruence, which contributes v ^ (p-1) - v rather than v ^ (p-1). So the bottom row is a v ^ (iLast)-row minus a multiple of an earlier row of the same matrix, and the relevant fact is that this row operation does not change the determinant.

Main results

• GranvilleMoore.det_of_eq_mul_pow_exponents: for an arbitrary exponent function f, the column scalars come out whole: det M = (∏ j, c j) * det (fun i j => v j ^ f i).
• GranvilleMoore.det_of_eq_mul_pow: the scaled Vandermonde determinant, f = id. The main result of the file: det M = (∏ j, c j) * ∏ i, ∏ j ∈ Ioi i, (v j - v i).
• GranvilleMoore.det_of_eq_mul_pow_ne_zero_iff and GranvilleMoore.det_of_eq_mul_pow_eq_zero_iff: over a domain, with all c j ≠ 0, the determinant is nonzero iff v is injective.
• GranvilleMoore.det_updateRow_sub_smul_self: subtracting a multiple of another row of the same matrix preserves the determinant (the d = p row operation).
• GranvilleMoore.det_of_eq_mul_pow_updateRow, ..._updateRow_last, ..._updateRow_sub: the one-row-modified variants, the last of which is the shape the d = p case produces.

Implementation notes

This file is deliberately free of project imports: nothing in it mentions p, a Fermat quotient, the Moore matrix or the ladder. The reduction is a statement about matrices over a commutative ring, so keeping it separate makes it reusable at every rung, keeps it immune to churn in the congruence files, and means the ladder lemmas can be wired to it independently of how the congruences are eventually proved.

Two Mathlib names behave contrary to their reading and are worth flagging: Matrix.det_mul_row is the one that scales columns ((fun i j => v j * A i j).det = (∏ i, v i) * A.det), and Matrix.det_mul_column is the one that scales rows. This file needs the column version, so it uses Matrix.det_mul_row.

Also note the index convention: Matrix.vandermonde v i j = v i ^ (j : ℕ) puts the power on the column index, whereas the entry shape arising from the ladder puts it on the row index. So the matrix here is the transpose of a Vandermonde matrix; Matrix.det_transpose bridges the two. In fact (Matrix.vandermonde v)ᵀ is definitionally Matrix.of fun i j => v j ^ (i : ℕ).

theorem GranvilleMoore.det_of_eq_mul_pow_exponents {R : Type u_1} [CommRing R] {n : ℕ} (c v : Fin n → R) (f : Fin n → ℕ) (M : Matrix (Fin n) (Fin n) R) (h : ∀ (i j : Fin n), M i j = c j * v j ^ f i) : M.det = (∏ j : Fin n, c j) * (Matrix.of fun (i j : Fin n) => v j ^ f i).det

If the entries of a square matrix factor as a column scalar times a power of a column value, the exponent depending only on the row — M i j = c j * v j ^ f i — then the column scalars factor out of the determinant all at once.

This is the general form: no relation between f and the row index is assumed, so the residual determinant is a generalized Vandermonde determinant rather than a product. Every other result in this file is a specialization.

theorem GranvilleMoore.det_of_eq_mul_pow {R : Type u_1} [CommRing R] {n : ℕ} (c v : Fin n → R) (M : Matrix (Fin n) (Fin n) R) (h : ∀ (i j : Fin n), M i j = c j * v j ^ ↑i) : M.det = (∏ j : Fin n, c j) * ∏ i : Fin n, ∏ j > i, (v j - v i)

The scaled Vandermonde determinant. If the entries of a square matrix over a commutative ring factor as M i j = c j * v j ^ (i : ℕ) — a scalar depending only on the column, times the column's value raised to the row index — then

det M = (∏ j, c j) * ∏ i, ∏ j ∈ Ioi i, (v j - v i).

The shape is what it is because such an M is (Matrix.vandermonde v)ᵀ with column j rescaled by c j: rescaling a column multiplies the determinant by that scalar, and transposing does not change it.

theorem GranvilleMoore.det_of_eq_mul_pow_ne_zero_iff {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] (c v : Fin n → R) (M : Matrix (Fin n) (Fin n) R) (hc : ∀ (j : Fin n), c j ≠ 0) (h : ∀ (i j : Fin n), M i j = c j * v j ^ ↑i) : M.det ≠ 0 ↔ Function.Injective v

The vanishing criterion. Over an integral domain, a matrix with entries c j * v j ^ (i : ℕ) and no vanishing column scalar has nonzero determinant exactly when the v j are pairwise distinct.

This is the form the main theorem needs: the p-adic valuation of the Moore determinant hits its lower bound iff the reduced last rung is invertible mod p, and that is a statement about the Fermat quotients being distinct.

theorem GranvilleMoore.det_of_eq_mul_pow_eq_zero_iff {R : Type u_1} [CommRing R] {n : ℕ} [IsDomain R] (c v : Fin n → R) (M : Matrix (Fin n) (Fin n) R) (hc : ∀ (j : Fin n), c j ≠ 0) (h : ∀ (i j : Fin n), M i j = c j * v j ^ ↑i) : M.det = 0 ↔ ∃ (i : Fin n) (j : Fin n), v i = v j ∧ i ≠ j

The contrapositive of GranvilleMoore.det_of_eq_mul_pow_ne_zero_iff, in the explicit "two coincident values" form.

theorem GranvilleMoore.det_updateRow_sub_smul_self {R : Type u_1} [CommRing R] {n : ℕ} (M : Matrix (Fin n) (Fin n) R) {i i₁ : Fin n} (hne : i ≠ i₁) (k : R) : (M.updateRow i fun (j : Fin n) => M i j - k * M i₁ j).det = M.det

Subtracting a multiple of another row of the same matrix from row i does not change the determinant. This is Matrix.det_updateRow_add_smul_self phrased with a subtraction and a ring multiplication, which is how the row operation of the d = p case actually presents itself.

theorem GranvilleMoore.det_of_eq_mul_pow_updateRow {R : Type u_1} [CommRing R] {n : ℕ} (c v : Fin n → R) (M : Matrix (Fin n) (Fin n) R) (iLast : Fin n) (e : ℕ) (h : ∀ (i j : Fin n), M i j = c j * v j ^ ↑i) : (M.updateRow iLast fun (j : Fin n) => c j * v j ^ e).det = (∏ j : Fin n, c j) * (Matrix.of fun (i j : Fin n) => v j ^ if i = iLast then e else ↑i).det

The one-row-modified variant. Replacing row iLast of a c j * v j ^ (i : ℕ) matrix by fun j => c j * v j ^ e still lets the column scalars out whole; what is left is the generalized Vandermonde determinant for the exponent list 0, 1, … with the entry at iLast replaced by e.

No further simplification is available in general: for e outside the original exponent list the residual determinant is a Schur polynomial times the Vandermonde product, not the Vandermonde product itself. The two cases that do collapse are GranvilleMoore.det_of_eq_mul_pow_updateRow_last and GranvilleMoore.det_of_eq_mul_pow_updateRow_sub.

theorem GranvilleMoore.det_of_eq_mul_pow_updateRow_last {R : Type u_1} [CommRing R] {n : ℕ} (c v : Fin (n + 1) → R) (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R) (h : ∀ (i j : Fin (n + 1)), M i j = c j * v j ^ ↑i) : (M.updateRow (Fin.last n) fun (j : Fin (n + 1)) => c j * v j ^ n).det = (∏ j : Fin (n + 1), c j) * ∏ i : Fin (n + 1), ∏ j > i, (v j - v i)

The special case of GranvilleMoore.det_of_eq_mul_pow_updateRow in which the modified exponent is the one the row already had, e = n - 1 in the last row: the determinant is the plain scaled Vandermonde determinant, so the caller can reduce to GranvilleMoore.det_of_eq_mul_pow.

theorem GranvilleMoore.det_of_eq_mul_pow_updateRow_sub {R : Type u_1} [CommRing R] {n : ℕ} (c v : Fin n → R) (M : Matrix (Fin n) (Fin n) R) {iLast i₁ : Fin n} (hne : iLast ≠ i₁) (k : R) (h : ∀ (i j : Fin n), M i j = c j * v j ^ ↑i) : (M.updateRow iLast fun (j : Fin n) => c j * (v j ^ ↑iLast - k * v j ^ ↑i₁)).det = (∏ j : Fin n, c j) * ∏ i : Fin n, ∏ j > i, (v j - v i)

The d = p shape. If the bottom row of a c j * v j ^ (i : ℕ) matrix is replaced by fun j => c j * (v j ^ (iLast : ℕ) - k * v j ^ (i₁ : ℕ)) for some other row index i₁, the determinant is unchanged, hence still the scaled Vandermonde determinant.

This is exactly what the exceptional Fermat congruence produces: it contributes x * q_p(x) ^ (p-1) - x * q_p(x) in the last row instead of x * q_p(x) ^ (p-1), i.e. the v ^ (iLast) row minus one copy of the v ^ 1 row, and a row operation of that form is determinant-preserving.