Commit 2021-05-31 13:18 2af69127

View on Github →

feat(linear_algebra): the determinant of an endomorphism (#7635) linear_map.det is the determinant of an endomorphism, which is defined independent of a basis. If there is no finite basis, the determinant is defined to be equal to 1. This approach is inspired by linear_map.trace.

Estimated changes

Modified docs/undergrad.yaml

Modified src/linear_algebra/determinant.lean

added theorem linear_map.coe_det

added def linear_map.det_aux

added theorem linear_map.det_aux_comp

added theorem linear_map.det_aux_def'

added theorem linear_map.det_aux_def

added theorem linear_map.det_aux_id

added theorem linear_map.det_comp

added theorem linear_map.det_eq_det_to_matrix_of_finite_set

added theorem linear_map.det_id

added theorem linear_map.det_to_matrix

added theorem linear_map.det_to_matrix_eq_det_to_matrix

added theorem linear_map.det_zero