Mathlib v3 is deprecated. Go to Mathlib v4

Theorem alternating_map.coe_add

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_add View on Github →