finite_of_det_ne_one — Mathlib

English

If the determinant of an endomorphism is not 1, then the module is finite.

Русский

Если детерминант эндоморфизма не равен 1, то модуль конечномерный.

LaTeX

$$$\det f \neq 1 \Rightarrow \mathrm{Module.Finite}\, R \ M$$$

Lean4

/-- If a linear map has determinant different from `1`, then the space is finite-dimensional. -/
theorem finite_of_det_ne_one {f : M →ₗ[R] M} (hf : f.det ≠ 1) : Module.Finite R M :=
  by
  by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)
  · rcases H with ⟨s, ⟨hs⟩⟩
    exact Module.Finite.of_basis hs
  · classical simp [LinearMap.coe_det, H] at hf

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