finrank_eq_rank' — Mathlib

English

In a finite-dimensional space, the finite-dimensional dimension equals the dimension as a cardinal.

Русский

В конечномерном пространстве размерность по основанию совпадает с размерностью как кардиналом.

LaTeX

$$(\operatorname{finrank}_K V : \mathrm{Cardinal}) = \mathrm{Module.rank}_K V$$

Lean4

/-- In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its
`finrank`. This is a copy of `finrank_eq_rank _ _` which creates easier typeclass searches. -/
theorem finrank_eq_rank' [FiniteDimensional K V] : (finrank K V : Cardinal.{v}) = Module.rank K V :=
  finrank_eq_rank _ _

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