finrank_finsupp_self — Mathlib

English

The finrank of Finsupp ι R is card ι when R is the scalar ring.

Русский

Конечная размерность Finsupp ι R равна кардиналу ι.

LaTeX

$$$\operatorname{finrank}_R(\mathrm{Finsupp}_{ι}(R)) = \operatorname{card}(ι)$$$

Lean4

/-- The `finrank` of `(ι →₀ R)` is `Fintype.card ι`. -/
@[simp]
theorem finrank_finsupp_self {ι : Type v} [Fintype ι] : finrank R (ι →₀ R) = card ι := by
  rw [finrank, rank_finsupp_self, ← mk_toNat_eq_card, toNat_lift]

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