mathlib

2af69127 - feat(linear_algebra): the determinant of an endomorphism (#7635)

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`. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>