Theorems · Definition · commutative algebra
IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime
{R : Type u_1} →
[inst : CommRing R] →
[IsDedekindDomain R] →
(K : Type u_2) →
[inst_2 : Field K] →
[inst_3 : Algebra R K] → [IsFractionRing R K] → IsDedekindDomain.HeightOneSpectrum R → ValuationSubring KGiven a Dedekind domain R in K, its field of fractions, the localization of R at
a nonzero prime is a valuation subring of K.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 135 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- Fieldstatement and proof · cited by 7,404
- IsFractionRingstatement and proof · cited by 738
- IsDedekindDomainstatement and proof · cited by 668
- Ideal.primeComplproof · cited by 462
- IsDedekindDomain.HeightOneSpectrumstatement and proof · cited by 338
- ValuationSubringstatement · cited by 187
- IsDedekindDomain.HeightOneSpectrum.asIdealproof · cited by 156
- Subalgebra.toSubringproof · cited by 30
- Localization.subalgebra.ofFieldproof · cited by 8
- ValuationSubring.ofSubringproof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- IsDedekindDomain.HeightOneSpectrum.exists_primeCompl_mul_eq_or_mul_eqproof · cited by 1
- IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_le_valuationstatement and proof · cited by 1
- IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime.congr_simpstatement and proof · cited by 0
- IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_eq_valuationSubringstatement and proof · cited by 0
- IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_toSubringstatement · cited by 0