English
If f is a continuous linear map with nonzero determinant on a finite-dimensional space, then f gives a continuous linear equivalence to itself (i.e., the determinant nonzero ensures invertibility in the continuous linear category).
Русский
Если линейное отображение непрерывно и имеет ненулевой детерминант на конечномерном пространстве, то оно дает непрерывно линейное эквивалентное отображение на себя (непосредственное инверсирование).
LaTeX
$$$\\forall f:\\, E \\to_L[𝕜] E,\\; f.\\det \\neq 0 \\Rightarrow f \\text{ is a continuous linear isomorphism}$$$
Lean4
/-- If `K` is a complete field and `V` is a finite-dimensional vector space over `K` (equipped with
any topology so that `V` is a topological `K`-module, meaning `[IsTopologicalAddGroup V]`
and `[ContinuousSMul K V]`), and `K` is locally compact, then `V` is locally compact.
This is not an instance because `K` cannot be inferred. -/
theorem of_finiteDimensional_of_complete (K V : Type*) [NontriviallyNormedField K] [CompleteSpace K]
[LocallyCompactSpace K] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module K V]
[ContinuousSMul K V] [FiniteDimensional K V] : LocallyCompactSpace V :=
-- Reduce to `SeparationQuotient V`, which is a `T2Space`.
suffices LocallyCompactSpace (SeparationQuotient V) from
SeparationQuotient.isInducing_mk.locallyCompactSpace <|
SeparationQuotient.range_mk (X := V) ▸ isClosed_univ.isLocallyClosed
let ⟨_, ⟨b⟩⟩ := Basis.exists_basis K (SeparationQuotient V)
have := FiniteDimensional.fintypeBasisIndex b
b.equivFun.toContinuousLinearEquiv.toHomeomorph.isOpenEmbedding.locallyCompactSpace
