rank_fun — Mathlib

English

For a finite index set η, finrank of the product ∀ i, M_i equals the sum of finranks: finrank_R(∀ i, M_i) = ∑_i 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

theorem rank_fun {M η : Type u} [Fintype η] [AddCommMonoid M] [Module R M] [Module.Free R M] :
    Module.rank R (η → M) = Fintype.card η * Module.rank R M := by
  rw [rank_pi, Cardinal.sum_const', Cardinal.mk_fintype]

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