vandermonde_apply

Mathlib.LinearAlgebra.Vandermonde

URI: https://scilib.ai/kg/mathlib#Matrix.vandermonde_apply

English

The (i,j) entry of vandermonde v is (v i)^j.

Русский

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

LaTeX

$$$\\mathrm{vandermonde}(v)_{i j} = (v(i))^{j}$$$

Lean4

@[simp]
theorem vandermonde_apply (v : Fin n → R) (i j) : vandermonde v i j = v i ^ (j : ℕ) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru