English
Let R be a commutative ring and n a natural number. For v,w : Fin(n+1) → R and i : Fin(n+1), if w(i) = 0, then the i-th row of the Vandermonde projection is the last standard basis vector scaled by (v(i))^n; equivalently, (projVandermonde v w) i equals the vector e_{last(n)} times (v(i))^n.
Русский
Пусть R — коммутативная кольцо, n — натуральное число. Для v, w : Fin(n+1) → R и i : Fin(n+1), если w(i) = 0, тогда i-я строка проекции Vandermonde равна последнему вектору базисной системы, умноженному на (v(i))^n; эквивалентно, (projVandermonde v w) i = e_{last(n)} (v(i))^n.
LaTeX
$$$ w i = 0 \\Rightarrow (\\mathrm{projVandermonde}\\, v\\, w)\\, i = \\Pi.select(\\mathrm{Fin.last}\\, n) \\big( (v i)^n \\big). $$$
Lean4
theorem projVandermonde_apply_zero_right {v w : Fin (n + 1) → R} {i : Fin (n + 1)} (hw : w i = 0) :
projVandermonde v w i = Pi.single (Fin.last n) ((v i) ^ n) :=
by
ext j
obtain rfl | hlt := j.le_last.eq_or_lt
· simp [projVandermonde_apply]
rw [projVandermonde_apply, Pi.single_eq_of_ne hlt.ne, hw, zero_pow, mul_zero]
simpa [Nat.sub_eq_zero_iff_le] using hlt
