Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-17 10:49 ee6969c3

View on Github →

chore(linear_algebra/{alternating,multilinear}): Add a handful of trivial lemmas (#5380) Some of these are needed for a WIP PR, and some seem like generally nice things to have.

Estimated changes