Documentation

Mathlib.Topology.Algebra.Module.Determinant

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