projVandermonde_apply_of_ne_zero — Mathlib

English

If w(i) ≠ 0, then (projVandermonde v w)_{i j} equals (v(i))^j * (w(i))^n / (w(i))^j.

Русский

При w(i) ≠ 0, (projVandermonde v w)_{i j} = (v(i))^j · (w(i))^n / (w(i))^j.

LaTeX

$$$\\mathrm{projVandermonde}(v,w,i,j) = (v(i))^{j} \\cdot (w(i))^{n} / (w(i))^{j}$ при $w(i) \\neq 0$$$

Lean4

theorem projVandermonde_apply_of_ne_zero {v w : Fin (n + 1) → K} {i j : Fin (n + 1)} (hw : w i ≠ 0) :
    projVandermonde v w i j = (v i) ^ j.1 * (w i) ^ n / (w i) ^ j.1 := by
  rw [projVandermonde_apply, eq_div_iff (by simp [hw]), mul_assoc, ← pow_add, rev_add_cast]

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