Vandermonde matrix #

This file defines the vandermonde matrix and gives its determinant.

Main definitions #

det_vandermonde: det (vandermonde v) is the product of v i - v j, where (i, j) ranges over the unordered pairs.

def matrix.vandermonde {R : Type u_1} [comm_ring R] {n : ℕ} (v : 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) :

theorem matrix.vandermonde_mul_vandermonde_transpose {R : Type u_1} [comm_ring R] {n : ℕ} (v w : fin n → R) (i j : fin n) :

theorem matrix.vandermonde_transpose_mul_vandermonde {R : Type u_1} [comm_ring R] {n : ℕ} (v : fin n → R) (i j : fin n) :

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)