English
If m and n are finite, the finrank of Matrix m n M equals card m × card n × finrank M.
Русский
Если m и n конечны, то finrank Matrix m n M равно card m × card n × finrank M.
LaTeX
$$$\operatorname{finrank}_R(\mathrm{Matrix}_{m,n}(M)) = \operatorname{card}(m) \cdot \operatorname{card}(n) \cdot \operatorname{finrank}_R M$$$
Lean4
/-- The `finrank` of a finite product is the sum of the `finrank`s. -/
theorem finrank_pi_fintype {ι : Type v} [Fintype ι] {M : ι → Type w} [∀ i : ι, AddCommMonoid (M i)]
[∀ i : ι, Module R (M i)] [∀ i : ι, Module.Free R (M i)] [∀ i : ι, Module.Finite R (M i)] :
finrank R (∀ i, M i) = ∑ i, finrank R (M i) := by
simp only [finrank, fun i => rank_eq_card_chooseBasisIndex R (M i), rank_pi, ← mk_sigma, mk_toNat_eq_card,
Fintype.card_sigma]
