The '''Vandermonde determinant of order n''' is the determinant defined as follows Vn=11⋮1x1x2⋮xnx12x22⋮xn2⋯⋯⋱⋯x1n−2x2n−2⋮xnn−2x1n−1x2n−1⋮xnn−1 Its value is given by Vn=1≤i<j≤n∏\parenxj−xi
theorem Vandermonde_Determinant {R : Type _} [CommRing R] {n : ℕ} (v : Fin n → R) : Matrix.det (Matrix.of fun i j : Fin n => v i ^ (j : ℕ)) = ∏ i : Fin n, ∏ j : Fin n, if i < j then v j - v i else 1 := by sorry