ofPrime

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

URI: https://scilib.ai/kg/mathlib#IsDedekindDomain.HeightOneSpectrum.ofPrime

Lean4

/-- The (nonzero) prime elements of the monoid with zero `Ideal R` correspond
to an element of type `HeightOneSpectrum R`.

See `IsDedekindDomain.HeightOneSpectrum.prime` for the inverse direction. -/
@[simps]
def ofPrime {p : Ideal R} (hp : Prime p) : HeightOneSpectrum R :=
  ⟨p, Ideal.isPrime_of_prime hp, hp.ne_zero⟩

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

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

Разделы

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

Аффилиация

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