finrank_eq_card_basis' — Mathlib

English

If V is finite-dimensional and h is a basis ι, then the cardinality of ι equals finrank_K V.

Русский

Если V конечномерно, и h является базисом с индексным множеством ι, то кардинал ι равен finrank_K V.

LaTeX

$$(\mathrm{finrank}_K V : \mathrm{Cardinal}) = \#ι$$

Lean4

/-- If a vector space is finite-dimensional, then the cardinality of any basis is equal to its
`finrank`. -/
theorem finrank_eq_card_basis' [FiniteDimensional K V] {ι : Type w} (h : Basis ι K V) :
    (finrank K V : Cardinal.{w}) = #ι :=
  Module.mk_finrank_eq_card_basis h

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