rectVandermonde_apply_zero_right — Mathlib

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

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