Theorem alternating_map.to_multilinear_map_alternization
Modification history
2020-12-17 10:49
src/linear_algebra/alternating.lean
chore(linear_algebra/{alternating,multilinear}): Add a handful of trivial lemmas (#5380) …
Deleted alternating_map.to_multilinear_map_alternizationView on Github →