finrank_pi — Mathlib

English

The rank of a finite product of modules is the sum of the ranks: rank_R(∀ i, φ i) = sum_i rank_R(φ i).

Русский

Ранг конечного произведения модулей равен сумме рангов модулей: rank(∀ i, φ i) = Σ_i rank(φ i).

LaTeX

$$$\operatorname{rank}_R\Bigl(\forall i, M_i\Bigr) = \sum_{i} \operatorname{rank}_R(M_i)$$$

Lean4

/-- The `finrank` of `(ι → R)` is `Fintype.card ι`. -/
theorem finrank_pi {ι : Type v} [Fintype ι] : finrank R (ι → R) = Fintype.card ι := by
  simp [finrank]
    --TODO: this should follow from `LinearEquiv.finrank_eq`, that is over a field.

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