Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_map.finite_dimensional_of_det_ne_one

Modification history

2021-12-18 20:11

src/linear_algebra/determinant.lean

feat(linear_algebra/determinant): more properties of the determinant of linear maps (#10809)

Added linear_map.finite_dimensional_of_det_ne_one View on Github →