coe_finsetBasisIndex — Mathlib

English

Let K be a division ring and V a Noetherian K-module. Then the finite basis indexed by finsetBasisIndex K V coincides, as a set of vectors, with the standard vector-space basis index Basis.ofVectorSpaceIndex K V.

Русский

Пусть K — деление кольца, а V — Noetherian K-модуль. Тогда множество индексов конечного базиса, задаваемое finsetBasisIndex K V, совпадает с обычным индексом базиса Basis.ofVectorSpaceIndex K V.

LaTeX

$$$ (\\uparrow(\\mathrm{finsetBasisIndex}\\,K\\,V) : \\mathrm{Set}\\,V) = \\mathrm{Basis.ofVectorSpaceIndex}\\,K\\,V $$$

Lean4

@[simp]
theorem coe_finsetBasisIndex [IsNoetherian K V] : (↑(finsetBasisIndex K V) : Set V) = Basis.ofVectorSpaceIndex K V :=
  Set.Finite.coe_toFinset _

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