English
For v,w : Fin n → R with R a commutative ring and n a natural number, the determinant of the projection matrix projVandermonde v w equals the product over i from 0 to n-1 and over j > i of (v(j)·w(i) − v(i)·w(j)).
Русский
Для v,w : Fin n → R, детерминант матрицы projVandermonde v w равен произведению по всем парам i<j из Fin n of (v(j)·w(i) − v(i)·w(j)).
LaTeX
$$$ (\\mathrm{projVandermonde}\\, v\\, w).det = \\prod i : Fin n, \\prod j ∈ Finset.Ioi i, (v j * w i - v i * w j). $$$
Lean4
/-- The formula for the determinant of a projective Vandermonde matrix. -/
theorem det_projVandermonde (v w : Fin n → R) :
(projVandermonde v w).det = ∏ i : Fin n, ∏ j ∈ Finset.Ioi i, (v j * w i - v i * w j) :=
by
let u (b : Bool) (i : Fin n) :=
(algebraMap (MvPolynomial (Fin n × Bool) ℤ) (FractionRing (MvPolynomial (Fin n × Bool) ℤ))) (MvPolynomial.X ⟨i, b⟩)
have hdet := det_projVandermonde_of_field (u true) (u false)
simp only [u] at hdet
norm_cast at hdet
rw [projVandermonde_map, ← RingHom.map_det, IsFractionRing.coe_inj] at hdet
apply_fun MvPolynomial.eval₂Hom (Int.castRingHom R) (fun x ↦ (if x.2 then v else w) x.1) at hdet
rw [RingHom.map_det] at hdet
convert hdet <;> simp [← Matrix.ext_iff, projVandermonde_apply]
