mathlib3 documentation

linear_algebra.vandermonde

Vandermonde matrix #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.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 = finset.univ.prod (λ (i : fin n), (finset.Ioi i).prod (λ (j : fin n), v j - v i))
theorem matrix.det_vandermonde_eq_zero_iff {R : Type u_1} [comm_ring R] [is_domain R] {n : } {v : fin n R} :
(matrix.vandermonde v).det = 0 (i j : fin n), v i = v j i j
theorem matrix.eq_zero_of_forall_index_sum_pow_mul_eq_zero {R : Type u_1} [comm_ring R] [is_domain R] {n : } {f v : fin n R} (hf : function.injective f) (hfv : (j : fin n), finset.univ.sum (λ (i : fin n), f j ^ i * v i) = 0) :
v = 0
theorem matrix.eq_zero_of_forall_index_sum_mul_pow_eq_zero {R : Type u_1} [comm_ring R] [is_domain R] {n : } {f v : fin n R} (hf : function.injective f) (hfv : (j : fin n), finset.univ.sum (λ (i : fin n), v i * f j ^ i) = 0) :
v = 0
theorem matrix.eq_zero_of_forall_pow_sum_mul_pow_eq_zero {R : Type u_1} [comm_ring R] [is_domain R] {n : } {f v : fin n R} (hf : function.injective f) (hfv : (i : fin n), finset.univ.sum (λ (j : fin n), v j * f j ^ i) = 0) :
v = 0