finrank_finsupp — Mathlib

English

For ι a finite type, finrank of Finsupp ι M equals card ι times finrank M.

Русский

Для конечного ι: finrank Finsupp ι M = card ι × finrank M.

LaTeX

$$$\operatorname{finrank}_R(\mathrm{Finsupp}_{\,ι}(M)) = \operatorname{card}(ι) \cdot \operatorname{finrank}_R M$$$

Lean4

@[simp]
theorem finrank_finsupp {ι : Type v} [Fintype ι] : finrank R (ι →₀ M) = card ι * finrank R M := by
  rw [finrank, finrank, rank_finsupp, ← mk_toNat_eq_card, toNat_mul, toNat_lift, toNat_lift]

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