English
The rank of a direct sum equals the sum of the ranks: rank_R(⊞_{i∈I} M_i) = ∑_{i∈I} rank_R(M_i).
Русский
Ранг прямой суммы равен сумме рангов: rank_R(DirectSum_i M_i) = Σ_i rank_R(M_i).
LaTeX
$$$\operatorname{rank}_R\Bigl(\bigoplus_{i\in I} M_i\Bigr) = \sum_{i\in I} \operatorname{rank}_R(M_i)$$$
Lean4
/-- The rank of the direct sum is the sum of the ranks. -/
@[simp]
theorem rank_directSum {ι : Type v} (M : ι → Type w) [∀ i : ι, AddCommMonoid (M i)] [∀ i : ι, Module R (M i)]
[∀ i : ι, Module.Free R (M i)] : Module.rank R (⨁ i, M i) = Cardinal.sum fun i => Module.rank R (M i) :=
by
let B i := chooseBasis R (M i)
let b : Basis _ R (⨁ i, M i) := DFinsupp.basis fun i => B i
simp [← b.mk_eq_rank'', fun i => (B i).mk_eq_rank'']
