Theorems · Inductive type · commutative algebra
IsDedekindDomain.HeightOneSpectrum
(R : Type u_1) → [CommRing R] → Type u_1
The height one prime spectrum of a Dedekind domain R is the type of nonzero prime ideals of
R. Note that this equals the maximal spectrum if R has Krull dimension 1.
- Cited by
- 338 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement · cited by 17,173
Cited by415
Results whose statement or proof uses this declaration.
- IsDedekindDomain.HeightOneSpectrum.asIdealstatement and proof · cited by 156
- IsDedekindDomain.HeightOneSpectrum.valuationstatement and proof · cited by 130
- IsDedekindDomain.HeightOneSpectrum.adicCompletionstatement · cited by 93
- IsDedekindDomain.HeightOneSpectrum.intValuationstatement and proof · cited by 53
- NumberField.FinitePlaceproof · cited by 35
- IsDiscreteValuationRing.maximalIdealstatement · cited by 25
- IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletionstatement and proof · cited by 25
- FractionalIdeal.countstatement and proof · cited by 25
- NumberField.FinitePlace.embeddingstatement and proof · cited by 24
- IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMapstatement and proof · cited by 23
- Polynomial.idealXstatement · cited by 23
- IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegersstatement and proof · cited by 22
Showing the 200 most cited of 415.