minimalPrimes_eq_setOf_isMaximal

Mathlib.RingTheory.KrullDimension.Zero

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

← MathLib Explorer

English

In a zero-dimensional ring, minimal primes coincide with maximal primes.

Русский

В кольце нулевой размерности минимальные-primes совпадают с максимальными-primes.

LaTeX

$$$\\text{minimalPrimes } R = \\{ I \\mid I.IsMaximal\\}$$$

Lean4

theorem minimalPrimes_eq_setOf_isMaximal : minimalPrimes R = {I | I.IsMaximal} := by ext;
  simp [minimalPrimes_eq_setOf_isPrime, Ideal.isMaximal_iff_isPrime]

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

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

Разделы

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

Аффилиация

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