Mathlib v3 is deprecated. Go to Mathlib v4

Theorem alternating_map.coe_zero

Modification history

2020-12-17 10:49

src/linear_algebra/alternating.lean

chore(linear_algebra/{alternating,multilinear}): Add a handful of trivial lemmas (#5380) …

Added alternating_map.coe_zero View on Github →