English
If w(i) = 0, then the (n+1)-th column of rectVandermonde with v is zero except at the last column, where it is (v(i))^n.
Русский
Если w(i)=0, то последняя колонка rectVandermonde содержит (v(i))^n, все прочие — нули.
LaTeX
$$$\\forall i, w(i)=0 \\Rightarrow \\mathrm{rectVandermonde}(v,w,n+1)_{i} = \\mathrm{Pi}.single(\\mathrm{Fin.last}\,n)\\, (v(i))^{n}$$$
Lean4
theorem rectVandermonde_apply_zero_right {α : Type*} {v w : α → R} {i : α} (hw : w i = 0) :
rectVandermonde v w (n + 1) i = Pi.single (Fin.last n) ((v i) ^ n) :=
by
ext j
obtain rfl | hlt := j.le_last.eq_or_lt
· simp [rectVandermonde_apply]
rw [rectVandermonde_apply, Pi.single_eq_of_ne hlt.ne, hw, zero_pow, mul_zero]
simpa [Nat.sub_eq_zero_iff_le] using hlt