mathlib documentation

topology.algebra.module.determinant

The determinant of a continuous linear map. #

@[reducible]
noncomputable def continuous_linear_map.det {R : Type u_1} [comm_ring R] {M : Type u_2} [topological_space M] [add_comm_group 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
@[simp]
theorem continuous_linear_equiv.det_coe_symm {R : Type u_1} [field R] {M : Type u_2} [topological_space M] [add_comm_group M] [module R M] (A : M ≃L[R] M) :