det_vandermonde_sub — Mathlib

English

For any v : Fin n → R and a ∈ R, det(vandermonde(v i − a)) = det(vandermonde(v)).

Русский

Для любого v : Fin n → R и a ∈ R, det(vandermonde(v i − a)) = det(vandermonde(v)).

LaTeX

$$$ \\det(\\mathrm{vandermonde}(\\lambda i. v i - a)) = \\det(\\mathrm{vandermonde}(v)). $$$

Lean4

@[simp]
theorem det_vandermonde_sub (v : Fin n → R) (a : R) :
    (Matrix.vandermonde fun i ↦ v i - a).det = (Matrix.vandermonde v).det :=
  by
  rw [← det_vandermonde_add v (-a)]
  simp only [← sub_eq_add_neg]

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