projVandermonde_apply — Mathlib

English

The (i,j)-entry of projVandermonde v w equals (v i)^j * (w i)^(j.rev).

Русский

Элемент (i,j) матрицы projVandermonde равен (v(i))^j · (w(i))^(j.rev).

LaTeX

$$$\\mathrm{projVandermonde}(v,w,n)_{i j} = (v(i))^{j} \\cdot (w(i))^{j.rev}$$$

Lean4

/-- We don't mark this as `@[simp]` because the RHS is not simp-nf,
and simplifying the RHS gives a bothersome `Nat` subtraction. -/
theorem projVandermonde_apply {v w : Fin n → R} {i j : Fin n} :
    projVandermonde v w i j = (v i) ^ j.1 * (w i) ^ j.rev.1 :=
  rfl

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