det_vandermonde_add — 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_add (v : Fin n → R) (a : R) :
    (Matrix.vandermonde fun i ↦ v i + a).det = (Matrix.vandermonde v).det := by simp [Matrix.det_vandermonde]

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