Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_map.bot_lt_ker_of_det_eq_zero

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.bot_lt_ker_of_det_eq_zero View on Github →