English
For a domain R and a function v : Fin n → R, det(vandermonde v) = 0 if and only if there exist i ≠ j with v(i) = v(j).
Русский
Для области R и функции v : Fin n → R, det(vandermonde v) = 0 тогда и только если существуют i ≠ j такие, что v(i) = v(j).
LaTeX
$$$ \\det(\\mathrm{vandermonde} v) = 0 \\iff \\exists i j : Fin n, v i = v j \\land i \\neq j. $$$
Lean4
theorem det_vandermonde_eq_zero_iff [IsDomain R] {v : Fin n → R} :
det (vandermonde v) = 0 ↔ ∃ i j : Fin n, v i = v j ∧ i ≠ j :=
by
constructor
· simp only [det_vandermonde v, Finset.prod_eq_zero_iff, sub_eq_zero, forall_exists_index]
rintro i ⟨_, j, h₁, h₂⟩
exact ⟨j, i, h₂, (mem_Ioi.mp h₁).ne'⟩
· simp only [Ne, forall_exists_index, and_imp]
refine fun i j h₁ h₂ => Matrix.det_zero_of_row_eq h₂ (funext fun k => ?_)
rw [vandermonde_apply, vandermonde_apply, h₁]
