Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-12 23:25 b9f24408

View on Github →

chore(linear_algebra/orientation): golf a proof (#10742)

Estimated changes

Modified src/linear_algebra/determinant.lean

added theorem alternating_map.map_basis_eq_zero_iff

added theorem alternating_map.map_basis_ne_zero_iff

Modified src/linear_algebra/orientation.lean