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

theorem ContinuousLinearMap.det_pi {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Fintype ι] [CommRing R] [AddCommGroup M] [TopologicalSpace M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : ι → M →L[R] M) : (pi fun (i : ι) => (f i).comp (proj i)).det = ∏ i : ι, (f i).det

@[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⁻¹