length_eq_coheight

Mathlib.RingTheory.Length

URI: https://scilib.ai/kg/mathlib#Module.length_eq_coheight

← MathLib Explorer

English

The length of a module equals the coheight of the zero submodule.

Русский

Длина модуля равна ко-высоте нулевого подмодуля.

LaTeX

$$$\operatorname{length}(R,M) = \operatorname{coheight}(\bot : \text{Submodule}_R M).$$$

Lean4

theorem length_eq_coheight : Module.length R M = Order.coheight (⊥ : Submodule R M) :=
  by
  apply WithBot.coe_injective
  rw [Module.coe_length, Order.coheight_bot_eq_krullDim]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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