Commit 2023-04-24 14:36 55815647

View on Github →

feat: port LinearAlgebra.Vandermonde (#3596)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Vandermonde.lean

added theorem Matrix.det_vandermonde

added theorem Matrix.det_vandermonde_eq_zero_iff

added theorem Matrix.det_vandermonde_ne_zero_iff

added theorem Matrix.eq_zero_of_forall_index_sum_mul_pow_eq_zero

added theorem Matrix.eq_zero_of_forall_index_sum_pow_mul_eq_zero

added theorem Matrix.eq_zero_of_forall_pow_sum_mul_pow_eq_zero

added def Matrix.vandermonde

added theorem Matrix.vandermonde_apply

added theorem Matrix.vandermonde_cons

added theorem Matrix.vandermonde_mul_vandermonde_transpose

added theorem Matrix.vandermonde_succ

added theorem Matrix.vandermonde_transpose_mul_vandermonde