of_fintype_basis — Mathlib

English

If a vector space has a finite basis, then it is finite-dimensional.

Русский

Если у пространства есть конечная база, то оно конечномерно.

LaTeX

$$$\text{FiniteDimensional } F V \Leftarrow \exists B:\ Basis\text{ finite}(B) $$$

Lean4

/-- If a vector space has a finite basis, then it is finite-dimensional. -/
theorem of_fintype_basis {ι : Type w} [Finite ι] (h : Basis ι K V) : FiniteDimensional K V :=
  Module.Finite.of_basis h

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