det_eq_one_of_not_module_finite — Mathlib

English

If M is not finite as an R-module, then det f = 1 for every endomorphism f.

Русский

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

LaTeX

$$$\text{If } \neg \mathrm{Module.Finite}\, R\, M, \text{ then } \det f = 1 \text{ for all } f \in \mathrm{End}_R(M).$$$

Lean4

theorem det_eq_one_of_not_module_finite (h : ¬Module.Finite R M) (f : M →ₗ[R] M) : f.det = 1 :=
  by
  rw [LinearMap.det, dif_neg, MonoidHom.one_apply]
  exact fun ⟨_, ⟨b⟩⟩ ↦ h (Module.Finite.of_basis b)

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