rank_finsupp' — Mathlib

English

The rank of ι →₀ M equals lift(#ι) times rank_R M, i.e., the dimension grows with the index set.

Русский

Ранг ι →₀ M равен lift(#ι) умноженному на ранг_R M; размерность растет с размером множества индексов.

LaTeX

$$$\operatorname{rank}_R(\iota \to_0 M) = \operatorname{lift}(\#\iota) \cdot \operatorname{rank}_R M$$$

Lean4

theorem rank_finsupp' (ι : Type v) : Module.rank R (ι →₀ M) = #ι * Module.rank R M := by simp [rank_finsupp]

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