det_eval_matrixOfPolynomials_eq_det_vandermonde

English

If deg(p_i) = i and p_i are monic, then det Vandermonde(v) equals the det of the evaluation matrix (p_j(v_i)).

Русский

Если степенность полиномов p_i satisfy deg(p_i) = i и p_i моничны, то det Vandermonde(v) равен детерминанту матрицы значений (p_j(v_i)).

LaTeX

$$$\\det(\\operatorname{vandermonde}(v)) = \\det\\left(\\big((p_j(v_i))\\big)_{i,j}\\right).$$$

Lean4

theorem det_eval_matrixOfPolynomials_eq_det_vandermonde (v : Fin n → R) (p : Fin n → R[X])
    (h_deg : ∀ i, (p i).natDegree = i) (h_monic : ∀ i, Monic <| p i) :
    (Matrix.vandermonde v).det = (Matrix.of (fun i j => ((p j).eval (v i)))).det := by
  rw [Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials v p (fun i ↦ Nat.le_of_eq (h_deg i)),
    Matrix.det_mul, Matrix.det_matrixOfPolynomials p h_deg h_monic, mul_one]

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