Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-05 18:50 52268b89

View on Github →

feat(linear_algebra): Vandermonde matrices and their determinant (#7116) This PR defines the vandermonde matrix and gives a formula for its determinant. @paulvanwamelen: if you would like to have det_vandermonde in a different form (e.g. swap the order of the variables that are being summed), please let me know!

Estimated changes