The determinant of a continuous linear map.

@[reducible]

noncomputable def ContinuousLinearMap.det {R : Type u_1} [CommRing R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup 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

• ContinuousLinearMap.det A = LinearMap.det ↑A

@[simp]

theorem ContinuousLinearEquiv.det_coe_symm {R : Type u_1} [Field R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] (A : M ≃L[R] M) : ContinuousLinearMap.det ↑(ContinuousLinearEquiv.symm A) = (ContinuousLinearMap.det ↑A)⁻¹