Theorems · Definition · functional analysis

ContinuousLinearMap.det

{R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : TopologicalSpace M] → [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → (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.

Defined in

Mathlib.Topology.Algebra.Module.Determinant

Cited by

44 results in Mathlib

Foundations

Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingTopologicalSpaceAddCommGroupModule