English
From a linear map with nonzero determinant (over a finite-dimensional space), one can build a linear equivalence.
Русский
Из линейного отображения с ненулевым детерминантом можно построить линейное эквивалентное отображение.
LaTeX
$$$\text{equivOfDetNeZero} : (\det f) \neq 0 \Rightarrow M \simeq M$$$
Lean4
/-- Builds a linear equivalence from a linear map on a finite-dimensional vector space whose
determinant is nonzero. -/
abbrev equivOfDetNeZero {𝕜 : Type*} [Field 𝕜] {M : Type*} [AddCommGroup M] [Module 𝕜 M] [FiniteDimensional 𝕜 M]
(f : M →ₗ[𝕜] M) (hf : LinearMap.det f ≠ 0) : M ≃ₗ[𝕜] M :=
have : IsUnit (LinearMap.toMatrix (Module.finBasis 𝕜 M) (Module.finBasis 𝕜 M) f).det :=
by
rw [LinearMap.det_toMatrix]
exact isUnit_iff_ne_zero.2 hf
LinearEquiv.ofIsUnitDet this
