rank_finsupp_self' — Mathlib

English

If R and the index type ι lie in the same universe, the rank of the finitely supported functions from ι to R, i.e., ι →₀ R, equals the cardinality of ι.

Русский

Если R и множество индексов ι живут в одной вселенной, ранг модуля конечной силы функций ι →₀ R равен кардинальному числу ι.

LaTeX

$$$ \\operatorname{rank}_R(\\iota \\to\\!_{0} R) = |\\iota| $$$

Lean4

/-- If `R` and `ι` lie in the same universe, the rank of `(ι →₀ R)` is `# ι`. -/
theorem rank_finsupp_self' {ι : Type u} : Module.rank R (ι →₀ R) = #ι := by simp

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