Determinant of the descending-Pochhammer evaluation matrix

The determinant of the matrix whose (i, j) entry is (descPochhammer ℂ j).eval (y i) is the Vandermonde product ∏ i, ∏ j ∈ Ioi i, (y j - y i).

This follows from the Mathlib theorem det_eval_matrixOfPolynomials_eq_det_vandermonde applied to the descending Pochhammer polynomials (which are monic of the correct degree) combined with det_vandermonde.

theorem RS.det_descPochhammer_eval {k : ℕ} (y : Fin k → ℂ) : (Matrix.of fun (i j : Fin k) => Polynomial.eval (y i) (descPochhammer ℂ ↑j)).det = ∏ i : Fin k, ∏ j > i, (y j - y i)

The descending-Pochhammer evaluation matrix has the Vandermonde determinant, the Pochhammers being monic of the right degrees.