det_vandermonde — Mathlib

English

Let v : Fin n → R. The determinant of the Vandermonde matrix built from v is the product over i of the product over j ∈ Ioi i of (v(j) − v(i)).

Русский

Пусть v : Fin n → R.Determinant матрицы Vandermonde, построенной по v, равен произведению по всем i и всем j > i из Fin n: (v(j) − v(i)).

LaTeX

$$$ \\det(\\mathrm{vandermonde}\\, v) = \\prod i : Fin n, \\prod j ∈ \\mathrm{Finset.Ioi}\\, i, (v j - v i). $$$

Lean4

/-- The formula for the determinant of a Vandermonde matrix. -/
theorem det_vandermonde (v : Fin n → R) : det (vandermonde v) = ∏ i : Fin n, ∏ j ∈ Ioi i, (v j - v i) := by
  simp [vandermonde_eq_projVandermonde, det_projVandermonde]

Похожие утверждения