FiniteDimensional — Mathlib

English

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

Русский

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

LaTeX

$$$\text{Basis }\mathcal{B} \Rightarrow \operatorname{FiniteDimensional} F V$$$

Lean4

/-- `FiniteDimensional` vector spaces are defined to be finite modules.
Use `FiniteDimensional.of_fintype_basis` to prove finite dimension from another definition. -/
abbrev FiniteDimensional (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V] :=
  Module.Finite K V

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