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.
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.