finrank_fintype_fun_eq_card — Mathlib

English

For a finite index η, the finrank of η → R equals the cardinality of η.

Русский

Для конечного множества индексов η размерность по основанию R пространства функций η → R равна мощности η.

LaTeX

$$$ \\operatorname{finrank} R (\\eta \\to R) = Fintype.card \\eta. $$$

Lean4

/-- The vector space of functions on a `Fintype ι` has `finrank` equal to the cardinality of `ι`. -/
@[simp]
theorem finrank_fintype_fun_eq_card : finrank R (η → R) = Fintype.card η :=
  finrank_eq_of_rank_eq rank_fun'

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