finiteDimensional — Mathlib

English

If there is an affine basis indexed by a finite set ι, then the underlying vector space V is finite-dimensional over k.

Русский

Если существует аффинная база, индексируемая конечным множеством ι, то связанное векторное пространство V конечноразмерно над полем k.

LaTeX

$$FiniteDimensional k V$$

Lean4

protected theorem finiteDimensional [Finite ι] (b : AffineBasis ι k P) : FiniteDimensional k V :=
  let ⟨i⟩ := b.nonempty
  FiniteDimensional.of_fintype_basis (b.basisOf i)

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