rank_finsupp_self

Mathlib.LinearAlgebra.Dimension.Constructions

URI: https://scilib.ai/kg/mathlib#rank_finsupp_self

English

Special case: rank of ι →₀ R equals #ι.

Русский

Специальный случай: ранг ι →₀ R равен #ι.

LaTeX

$$$\operatorname{rank}_R(\iota \to_0 R) = \#\iota$$$

Lean4

/-- The rank of `(ι →₀ R)` is `(#ι).lift`. -/
theorem rank_finsupp_self (ι : Type w) : Module.rank R (ι →₀ R) = Cardinal.lift.{u} #ι := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru