English
For a finite η, finrank_R(∀ i, M_i) equals the sum over i of finrank_R(M_i).
Русский
Пусть η конечно: finrank R(∀ i, M_i) = сумма finrank R(M_i).
LaTeX
$$$\operatorname{finrank}_R\Bigl(\forall i, M_i\Bigr) = \sum_{i} \operatorname{finrank}_R(M_i)$$$
Lean4
/-- The rank of a finite product of free modules is the sum of the ranks. -/
-- this result is not true without the freeness assumption
@[simp]
theorem rank_pi [Finite η] : Module.rank R (∀ i, φ i) = Cardinal.sum fun i => Module.rank R (φ i) :=
by
cases nonempty_fintype η
let B i := chooseBasis R (φ i)
let b : Basis _ R (∀ i, φ i) := Pi.basis fun i => B i
simp [← b.mk_eq_rank'', fun i => (B i).mk_eq_rank'']
