The determinant of a continuous linear map. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[reducible]
noncomputable
def
continuous_linear_map.det
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[topological_space M]
[add_comm_group M]
[module R M]
(A : M →L[R] M) :
R
The determinant of a continuous linear map, mainly as a convenience device to be able to
write A.det instead of (A : M →ₗ[R] M).det.
Equations
- A.det = ⇑linear_map.det ↑A