English
The finrank of a direct sum equals the sum of the finranks: finrank_R(DirectSum_i M_i) = sum_i finrank_R(M_i).
Русский
Финранк прямой суммы равен сумме финранков: finrank(DirectSum_i M_i) = сумма finrank(M_i).
LaTeX
$$$\operatorname{finrank}_R\Bigl(\bigoplus_{i} M_i\Bigr) = \sum_{i} \operatorname{finrank}_R(M_i)$$$
Lean4
/-- The `finrank` of the direct sum is the sum of the `finrank`s. -/
@[simp]
theorem finrank_directSum {ι : 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_directSum, ← mk_sigma, mk_toNat_eq_card,
card_sigma]
