coeSort_finsetBasisIndex — Mathlib

English

For Noetherian K,V, the type finsetBasisIndex K V is equal to the vector-space basis index type Basis.ofVectorSpaceIndex K V.

Русский

Для Noetherian K,V тип finsetBasisIndex K V равен типу индекса базиса векторного пространства Basis.ofVectorSpaceIndex K V.

LaTeX

$$$ (finsetBasisIndex K V : Type _) = Basis.ofVectorSpaceIndex K V $$$

Lean4

@[simp]
theorem coeSort_finsetBasisIndex [IsNoetherian K V] : (finsetBasisIndex K V : Type _) = Basis.ofVectorSpaceIndex K V :=
  Set.Finite.coeSort_toFinset _

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