mathlib documentation

linear_algebra.vandermonde

Vandermonde matrix #

This file defines the vandermonde matrix and gives its determinant.

Main definitions #

Main results #

def matrix.vandermonde {R : Type u_1} [comm_ring R] {n : } (v : fin n → R) :
matrix (fin n) (fin n) R

vandermonde v is the square matrix with ith row equal to 1, v i, v i ^ 2, v i ^ 3, ....

Equations
@[simp]
theorem matrix.vandermonde_apply {R : Type u_1} [comm_ring R] {n : } (v : fin n → R) (i j : fin n) :
@[simp]
theorem matrix.vandermonde_cons {R : Type u_1} [comm_ring R] {n : } (v0 : R) (v : fin n → R) :
matrix.vandermonde (fin.cons v0 v) = fin.cons (λ (j : fin (n + 1)), v0 ^ j) (λ (i : fin n), fin.cons 1 (λ (j : fin n), (v i) * matrix.vandermonde v i j))
theorem matrix.vandermonde_succ {R : Type u_1} [comm_ring R] {n : } (v : fin n.succ → R) :
matrix.vandermonde v = fin.cons (λ (j : fin n.succ), v 0 ^ j) (λ (i : fin n), fin.cons 1 (λ (j : fin n), (v i.succ) * matrix.vandermonde (fin.tail v) i j))
theorem matrix.det_vandermonde {R : Type u_1} [comm_ring R] {n : } (v : fin n → R) :
(matrix.vandermonde v).det = ∏ (i : fin n), ∏ (j : fin n) in finset.filter (λ (j : fin n), i < j) finset.univ, (v j - v i)