det_eq_one_of_finrank_eq_zero — Mathlib

English

For any field 𝕜 and M with finrank 𝕜 M = 0, det f = 1 for all endomorphisms f.

Русский

Для поля 𝕜 и пространства M с finrank = 0 детерминант любого эндоморфизма равен 1.

LaTeX

$$$\mathrm{finrank}_{\mathbb{k}} M = 0 \Rightarrow \det f = 1\quad\text{for all } f: M \to M$$$

Lean4

theorem det_eq_one_of_finrank_eq_zero {𝕜 : Type*} [Field 𝕜] {M : Type*} [AddCommGroup M] [Module 𝕜 M]
    (h : Module.finrank 𝕜 M = 0) (f : M →ₗ[𝕜] M) : LinearMap.det (f : M →ₗ[𝕜] M) = 1 := by
  classical
  refine @LinearMap.det_cases M _ 𝕜 _ _ _ (fun t => t = 1) f ?_ rfl
  intro s b
  have : IsEmpty s := by
    rw [← Fintype.card_eq_zero_iff]
    exact (Module.finrank_eq_card_basis b).symm.trans h
  exact Matrix.det_isEmpty

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