Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_map.det_cases

Modification history

2021-06-14 21:50
src/linear_algebra/determinant.lean
feat(linear_algebra/determinant): specialize `linear_equiv.is_unit_det` to automorphisms (#7667) …
Added linear_map.det_casesView on Github →