Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-13 16:19 3b4f4daf

View on Github →

feat(linear_algebra/determinant): more on the determinant of linear maps (#9139)

Estimated changes

Modified src/linear_algebra/determinant.lean

added theorem linear_map.det_conj

added theorem linear_map.det_smul

added theorem linear_map.det_to_matrix'

added theorem linear_map.det_zero'

modified theorem linear_map.det_zero

added def linear_map.equiv_of_det_ne_zero

Modified src/linear_algebra/matrix/to_lin.lean

added theorem linear_map.to_matrix_eq_to_matrix'

added theorem matrix.to_lin_eq_to_lin'