The determinant of a continuous linear map. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
The determinant of a continuous linear map, mainly as a convenience device to be able to
A.det instead of
(A : M →ₗ[R] M).det.