Theorems · Definition · commutative algebra

IsDedekindDomain.HeightOneSpectrum.ofPrime

{R : Type u_1} →
  [inst : CommRing R] → [IsDedekindDomain R] → {p : Ideal R} → Prime p → IsDedekindDomain.HeightOneSpectrum R

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.

Defined in

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Cited by

4 results in Mathlib

Foundations

Depth 148 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDedekindDomain