det_eq_one_of_subsingleton — Mathlib

English

If the (finite) dimension is zero, then det f = 1 for every endomorphism f over a field 𝕜.

Русский

Если размерность пространства равна нулю, то для любого эндоморфизма детерминант равен 1.

LaTeX

$$$\text{If } \mathrm{finrank}_{\mathbb{F}} M = 0, \text{ then } \det f = 1$ for all endomorphisms f.$$

Lean4

@[nontriviality]
theorem det_eq_one_of_subsingleton [Subsingleton M] (f : M →ₗ[R] M) : LinearMap.det (f : M →ₗ[R] M) = 1 :=
  by
  have b : Basis (Fin 0) R M := Basis.empty M
  rw [← f.det_toMatrix b]
  exact Matrix.det_isEmpty

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