det — Mathlib

English

For a continuous linear map A: M →L[R] M, the determinant is the same as the determinant of its underlying linear map.

Русский

Для непрерывного линейного отображения A: M →L[R] M детерминант совпадает с детерминантом соответствующего линейного отображения.

LaTeX

$$$\det(A) = \det(A: M \to M)$$$

Lean4

/-- 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`. -/
noncomputable abbrev det {R : Type*} [CommRing R] {M : Type*} [TopologicalSpace M] [AddCommGroup M] [Module R M]
    (A : M →L[R] M) : R :=
  LinearMap.det (A : M →ₗ[R] M)

Похожие утверждения