Documentation

Mathlib.LinearAlgebra.Vandermonde

Vandermonde matrix #

This file defines the vandermonde matrix and gives its determinant.

Main definitions #

Main results #

def Matrix.vandermonde {R : Type u_1} [CommRing R] {n : } (v : Fin nR) :
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
Instances For
    @[simp]
    theorem Matrix.vandermonde_apply {R : Type u_1} [CommRing R] {n : } (v : Fin nR) (i : Fin n) (j : Fin n) :
    Matrix.vandermonde v i j = v i ^ j
    @[simp]
    theorem Matrix.vandermonde_cons {R : Type u_1} [CommRing R] {n : } (v0 : R) (v : Fin nR) :
    Matrix.vandermonde (Fin.cons v0 v) = Fin.cons (fun j => v0 ^ j) fun i => Fin.cons 1 fun j => v i * Matrix.vandermonde v i j
    theorem Matrix.vandermonde_succ {R : Type u_1} [CommRing R] {n : } (v : Fin (Nat.succ n)R) :
    Matrix.vandermonde v = Fin.cons (fun j => v 0 ^ j) fun i => Fin.cons 1 fun j => v (Fin.succ i) * Matrix.vandermonde (Fin.tail v) i j
    theorem Matrix.vandermonde_mul_vandermonde_transpose {R : Type u_1} [CommRing R] {n : } (v : Fin nR) (w : Fin nR) (i : Fin n) (j : Fin n) :
    (Matrix (Fin n) (Fin n) R * Matrix (Fin n) (Fin n) R) (Matrix (Fin n) (Fin n) R) Matrix.instHMulMatrixMatrixMatrix (Matrix.vandermonde v) (Matrix.transpose (Matrix.vandermonde w)) i j = Finset.sum Finset.univ fun k => (v i * w j) ^ k
    theorem Matrix.vandermonde_transpose_mul_vandermonde {R : Type u_1} [CommRing R] {n : } (v : Fin nR) (i : Fin n) (j : Fin n) :
    (Matrix (Fin n) (Fin n) R * Matrix (Fin n) (Fin n) R) (Matrix (Fin n) (Fin n) R) Matrix.instHMulMatrixMatrixMatrix (Matrix.transpose (Matrix.vandermonde v)) (Matrix.vandermonde v) i j = Finset.sum Finset.univ fun k => v k ^ (i + j)
    theorem Matrix.det_vandermonde {R : Type u_1} [CommRing R] {n : } (v : Fin nR) :
    Matrix.det (Matrix.vandermonde v) = Finset.prod Finset.univ fun i => Finset.prod (Finset.Ioi i) fun j => v j - v i
    theorem Matrix.det_vandermonde_eq_zero_iff {R : Type u_1} [CommRing R] [IsDomain R] {n : } {v : Fin nR} :
    Matrix.det (Matrix.vandermonde v) = 0 i j, v i = v j i j
    @[simp]
    theorem Matrix.det_vandermonde_add {R : Type u_1} [CommRing R] {n : } (v : Fin nR) (a : R) :
    @[simp]
    theorem Matrix.det_vandermonde_sub {R : Type u_1} [CommRing R] {n : } (v : Fin nR) (a : R) :
    theorem Matrix.eq_zero_of_forall_index_sum_pow_mul_eq_zero {R : Type u_2} [CommRing R] [IsDomain R] {n : } {f : Fin nR} {v : Fin nR} (hf : Function.Injective f) (hfv : ∀ (j : Fin n), (Finset.sum Finset.univ fun i => f j ^ i * v i) = 0) :
    v = 0
    theorem Matrix.eq_zero_of_forall_index_sum_mul_pow_eq_zero {R : Type u_2} [CommRing R] [IsDomain R] {n : } {f : Fin nR} {v : Fin nR} (hf : Function.Injective f) (hfv : ∀ (j : Fin n), (Finset.sum Finset.univ fun i => v i * f j ^ i) = 0) :
    v = 0
    theorem Matrix.eq_zero_of_forall_pow_sum_mul_pow_eq_zero {R : Type u_2} [CommRing R] [IsDomain R] {n : } {f : Fin nR} {v : Fin nR} (hf : Function.Injective f) (hfv : ∀ (i : Fin n), (Finset.sum Finset.univ fun j => v j * f j ^ i) = 0) :
    v = 0