Mathlib v3 is deprecated. Go to Mathlib v4

Theorem basis.det_is_empty

Modification history

2023-05-30 03:49
src/linear_algebra/determinant.lean
chore(linear_algebra/alternating): make `ι` an explicit arg of `alternating_map.const_of_is_empty` (#19123) …
Modified basis.det_is_emptyView on Github →
2022-10-12 10:35
src/linear_algebra/determinant.lean
feat(analysis/inner_product_space/orientation): volume form (#16487) …
Added basis.det_is_emptyView on Github →