The determinant of a continuous linear map.

@[reducible, inline]

noncomputable abbrev 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

• A.det = 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) : (↑A.symm).det = (↑A).det⁻¹