supportDim_ne_bot_of_nontrivial

Mathlib.RingTheory.KrullDimension.Module

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

← MathLib Explorer

English

If M is nontrivial, then the Krull dimension of M is not bottom.

Русский

Если M не тривиален, то Krull размерность не равна ⊥.

LaTeX

$$$[\text{Nontrivial}(M)] \Rightarrow \operatorname{supportDim}(R,M) \neq \bot$$$

Lean4

theorem supportDim_ne_bot_of_nontrivial [Nontrivial M] : supportDim R M ≠ ⊥ := by
  simpa [supportDim, support_eq_empty_iff, not_subsingleton_iff_nontrivial]

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

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

Разделы

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

Аффилиация

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