basisOfFinrankZero — Mathlib

English

If ι is an empty type and V is zero-dimensional, there exists a basis of V indexed by ι, and it is unique (the empty basis).

Русский

Если ι пустого типа и V имеет нулевую размерность, существует база пространства V, индексируемая ι, и она единственна (пустая база).

LaTeX

$$$\text{If } ι \text{ is empty and } \operatorname{finrank}_K(V)=0, \text{ there exists a basis } B : \text{Basis } ι K V$$$

Lean4

/-- If `ι` is an empty type and `V` is zero-dimensional, there is a unique `ι`-indexed basis. -/
noncomputable def basisOfFinrankZero [FiniteDimensional K V] {ι : Type*} [IsEmpty ι] (hV : finrank K V = 0) :
    Basis ι K V :=
  haveI : Subsingleton V := finrank_zero_iff.1 hV
  Basis.empty _

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