Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-21 07:33 da6cd551

View on Github →

feat(determinant): towards multilinearity (#3887) From the sphere eversion project. In a PR coming soon, this will be used to prove that the determinant of a family of vectors in a given basis is multi-linear (see here for a preview if needed).

Estimated changes