English
vandermonde with cons recurses by prepending a new first column and shifting others; it satisfies a standard recurrence with pow and product rules.
Русский
Матрица Vandermonde с добавлением нового столбца строится по рекуррентной формуле с показателями степеней и произведениями.
LaTeX
$$$\\mathrm{vandermonde}(\\mathrm{Fin}.cons(v0,v)) = \\mathrm{Fin}.cons(\\lambda j. v0^{j})(\\lambda i. \\mathrm{Fin}.cons(1)(v(i) \\cdot \\mathrm{vandermonde}(v)(i)))$$$
Lean4
@[simp]
theorem vandermonde_cons (v0 : R) (v : Fin n → R) :
vandermonde (Fin.cons v0 v : Fin n.succ → R) =
Fin.cons (fun (j : Fin n.succ) => v0 ^ (j : ℕ)) fun i => Fin.cons 1 fun j => v i * vandermonde v i j :=
by
ext i j
refine Fin.cases (by simp) (fun i => ?_) i
refine Fin.cases (by simp) (fun j => ?_) j
simp [pow_succ']
