Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-18 20:11 9f1b9bcd

View on Github →

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

Estimated changes

Modified src/linear_algebra/determinant.lean

added theorem linear_equiv.det_coe_symm

added theorem linear_map.bot_lt_ker_of_det_eq_zero

added theorem linear_map.finite_dimensional_of_det_ne_one

added theorem linear_map.is_unit_det

added theorem linear_map.range_lt_top_of_det_eq_zero

Modified src/linear_algebra/eigenspace.lean

Modified src/linear_algebra/finite_dimensional.lean

deleted theorem linear_map.is_unit_iff

added theorem linear_map.is_unit_iff_ker_eq_bot

added theorem linear_map.is_unit_iff_range_eq_top