English
For any v : Fin(n+1) → Z, the integer ↑n.superFactorial divides det(vandermonde(v)).
Русский
Для любого v : Fin(n+1) → Z целая число ↑n.superFactorial делит det(vandermonde(v)).
LaTeX
$$$\\uparrow n.\\mathrm{superFactorial} \\; \\mid \\; \\det(\\operatorname{vandermonde}(v)).$$$
Lean4
theorem superFactorial_dvd_vandermonde_det {n : ℕ} (v : Fin (n + 1) → ℤ) : ↑n.superFactorial ∣ (vandermonde v).det :=
by
let m := inf' univ ⟨0, mem_univ _⟩ v
let w' := fun i ↦ (v i - m).toNat
have hw' : ∀ i, (w' i : ℤ) = v i - m := fun i ↦ Int.toNat_sub_of_le (inf'_le _ (mem_univ _))
have h :=
det_eval_matrixOfPolynomials_eq_det_vandermonde (fun i ↦ ↑(w' i)) (fun i => descPochhammer ℤ i)
(fun i => descPochhammer_natDegree ℤ i) (fun i => monic_descPochhammer ℤ i)
conv_lhs at h => simp only [hw', det_vandermonde_sub]
use (of (fun (i j : Fin (n + 1)) => (Nat.choose (w' i) (j : ℕ) : ℤ))).det
simp [h, of_eval_descPochhammer_eq_mul_of_choose w', Fin.prod_univ_eq_prod_range]
