Mathlib v3 is deprecated. Go to Mathlib v4

Theorem alternating_map.map_linear_dependent

Modification history

2021-01-03 02:24

src/linear_algebra/alternating.lean

feat(linear_algebra/alternating): Show the link to linear_independent (#5477)

Added alternating_map.map_linear_dependent View on Github →