rectVandermonde — Mathlib

English

rectVandermonde is the matrix with entries (v i)^j * (w i)^(j.rev).

Русский

rectVandermonde — матрица со скобочными элементами (v i)^j · (w i)^(j.rev).

LaTeX

$$$\\mathrm{rectVandermonde}(v,w,n)_{i j} = (v(i))^{j} \\cdot (w(i))^{j^{-1}}$$$

Lean4

/-- A matrix with rows all having the form `[b^(n-1), a * b^(n-2), ..., a ^ (n-1)]` -/
def rectVandermonde {α : Type*} (v w : α → R) (n : ℕ) : Matrix α (Fin n) R :=
  .of fun i j ↦ (v i) ^ j.1 * (w i) ^ j.rev.1

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