existsUnique_isPrime

Mathlib.RingTheory.KrullDimension.Zero

URI: https://scilib.ai/kg/mathlib#Ring.KrullDimLE.existsUnique_isPrime

← MathLib Explorer

English

Under local ring hypotheses, there exists a unique prime ideal.

Русский

При локальном кольце существует единственный примительный идеал.

LaTeX

$$$\\exists! I: \\text{Ideal } R, I.IsPrime$$$

Lean4

theorem existsUnique_isPrime [IsLocalRing R] : ∃! I : Ideal R, I.IsPrime :=
  ((Ring.krullDimLE_zero_and_isLocalRing_tfae R).out 0 1 rfl rfl).mp ⟨‹_›, ‹_›⟩

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

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

Разделы

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

Аффилиация

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