supportDim_eq_bot_iff_subsingleton

Mathlib.RingTheory.KrullDimension.Module

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

English

The equality supportDim(R,M) = ⊥ is equivalent to Subsingleton(M).

Русский

Равенство \operatorname{supportDim}(R,M) = ⊥ эквивалентно Subsingleton(M).

LaTeX

$$$\operatorname{supportDim}(R,M) = \bot \iff \text{Subsingleton}(M)$$$

Lean4

theorem supportDim_eq_bot_iff_subsingleton : supportDim R M = ⊥ ↔ Subsingleton M := by
  simp [supportDim, krullDim_eq_bot_iff, support_eq_empty_iff]

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

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

Разделы

Аффилиация

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