nonempty_minimalPrimes

Mathlib.RingTheory.Ideal.MinimalPrime.Basic

URI: https://scilib.ai/kg/mathlib#Ideal.nonempty_minimalPrimes

← MathLib Explorer

English

If I is not the top ideal, then I.minimalPrimes is nonempty.

Русский

Если I не равен верхнему идеалу, то I.minimalPrimes не пусто.

LaTeX

$$$I \neq \top \;\Rightarrow\; Nonempty(I.minimalPrimes)$$$

Lean4

theorem nonempty_minimalPrimes (h : I ≠ ⊤) : Nonempty I.minimalPrimes :=
  by
  obtain ⟨m, hm, hle⟩ := Ideal.exists_le_maximal I h
  obtain ⟨p, hp, -⟩ := Ideal.exists_minimalPrimes_le hle
  exact ⟨p, hp⟩

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

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

Разделы

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

Аффилиация

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