instFintypeElemOfVectorSpaceIndex

English

If V is finite-dimensional, then Basis.ofVectorSpaceIndex(K,V) is finite type.

Русский

Если V конечномерно над K, то индекс Basis.ofVectorSpaceIndex(K,V) является конечным типом.

LaTeX

$$FiniteDimensional(K,V) ⇒ Finite(Basis.ofVectorSpaceIndex(K,V))$$

Lean4

/-- If a vector space is `FiniteDimensional`, `Basis.ofVectorSpace` is indexed by
  a finite type. -/
noncomputable instance [FiniteDimensional K V] : Fintype (Basis.ofVectorSpaceIndex K V) :=
  fintypeBasisIndex (Basis.ofVectorSpace K V)

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