English
Let K,V be as above with IsNoetherian K V. Then there exists a finite basis for V obtained by reindexing the usual basis Basis.ofVectorSpace K V along the finite index finsetBasisIndex K V.
Русский
Пусть K,V удовлетворяют условиям; тогда существует конечный базис V, получаемый повторной нумерацией обычного базиса Basis.ofVectorSpace K V по конечному индексу IsNoetherian.finsetBasisIndex K V.
LaTeX
$$$\\mathrm{finsetBasis}(K,V) : \\mathrm{Basis}(\\mathrm{Subtype}(\\lambda x\\,\\, x\\in \\mathrm{IsNoetherian.finsetBasisIndex}\\,K\\,V))\\,K\\,V$$$
Lean4
/-- In a Noetherian module over a division ring, there exists a finite basis.
This is indexed by the `Finset` `IsNoetherian.finsetBasisIndex`.
This is in contrast to the result `finite_basis_index (Basis.ofVectorSpace K V)`,
which provides a set and a `Set.Finite`.
-/
noncomputable def finsetBasis [IsNoetherian K V] : Basis (finsetBasisIndex K V) K V :=
(Basis.ofVectorSpace K V).reindex (by rw [coeSort_finsetBasisIndex])
