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.

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

theorem ContinuousLinearMap.det_smulRight {𝕜 : Type u_1} [CommRing 𝕜] [TopologicalSpace 𝕜] [ContinuousMul 𝕜] (f : 𝕜 →L[𝕜] 𝕜) (v : 𝕜) : (f.smulRight v).det = f 1 * v

theorem ContinuousLinearMap.det_toSpanSingleton {𝕜 : Type u_1} [CommRing 𝕜] [TopologicalSpace 𝕜] [ContinuousMul 𝕜] (v : 𝕜) : (toSpanSingleton 𝕜 v).det = v

@[deprecated ContinuousLinearMap.det_toSpanSingleton (since := "2025-12-18")]

theorem ContinuousLinearMap.det_one_smulRight {𝕜 : Type u_1} [CommRing 𝕜] [TopologicalSpace 𝕜] [ContinuousMul 𝕜] (v : 𝕜) : (toSpanSingleton 𝕜 v).det = v

Alias of ContinuousLinearMap.det_toSpanSingleton.

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