finrank_prod — Mathlib

English

For a type ι and an R-module M, the rank of the finitely supported functions ι →₀ M is the product of lift(#ι) and lift(rank_R M).

Русский

Для типа ι и модуля M над R ранг Finsupp ι M равен произведению lift(#ι) и lift(ранг_R M).

LaTeX

$$$\operatorname{rank}_R(\iota \to\!\!_0 M) = \operatorname{lift}(\#\iota) \cdot \operatorname{lift}(\operatorname{rank}_R M)$$$

Lean4

/-- The `finrank` of `M × M'` is `(finrank R M) + (finrank R M')`. -/
@[simp]
theorem finrank_prod [Module.Finite R M] [Module.Finite R M'] : finrank R (M × M') = finrank R M + finrank R M' := by
  simp [finrank, rank_lt_aleph0 R M, rank_lt_aleph0 R M']

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