fintypeBasisIndex — Mathlib

English

If V is finite-dimensional, then any basis is indexed by a finite type.

Русский

Если V конечномерно, то любой базис индексируется конечным типом.

LaTeX

$$FiniteDimensional(K, V) ⇒ ∀ B: Basis, Finite B.Index$$

Lean4

/-- If a vector space is `FiniteDimensional`, all bases are indexed by a finite type -/
noncomputable def fintypeBasisIndex {ι : Type*} [FiniteDimensional K V] (b : Basis ι K V) : Fintype ι :=
  @Fintype.ofFinite _ (Module.Finite.finite_basis b)

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