coe_length

Mathlib.RingTheory.Length

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

English

The length is zero if and only if the module is subsingleton.

Русский

Длина равна нулю тогда и только тогда, когда модуль единично-тривиален (субоднозначный).

LaTeX

$$$\operatorname{length}(R,M) = 0 \iff \operatorname{Subsingleton} M.$$$

Lean4

theorem coe_length : (Module.length R M : WithBot ℕ∞) = Order.krullDim (Submodule R M) :=
  WithBot.coe_unbot _ _

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

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

Разделы

Аффилиация

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