Theorems · Definition · commutative algebra
ValuationSubring.ofPrime
{K : Type u} → [inst : Field K] → (A : ValuationSubring K) → (P : Ideal ↥A) → [P.IsPrime] → ValuationSubring KThe coarsening of a valuation ring associated to a prime ideal.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FieldIdeal.IsPrime
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fieldstatement and proof · cited by 7,404
- Idealstatement and proof · cited by 4,748
- Ideal.IsPrimestatement and proof · cited by 827
- Ideal.primeComplproof · cited by 462
- ValuationSubringstatement and proof · cited by 187
- Subalgebra.toSubringproof · cited by 30
- Localization.subalgebra.ofFieldproof · cited by 8
- ValuationSubring.ofLEproof · cited by 0
Cited by11
Results whose statement or proof uses this declaration.
- ValuationSubring.eq_self_or_eq_top_of_leproof · cited by 3
- ValuationSubring.le_ofPrimestatement · cited by 2
- ValuationSubring.ofPrime_idealOfLEstatement and proof · cited by 2
- ValuationSubring.primeSpectrumEquivproof · cited by 2
- ValuationSubring.ofPrime_botstatement · cited by 1
- ValuationSubring.ofPrime_topstatement · cited by 1
- ValuationSubring.primeSpectrumEquiv_applystatement · cited by 1
- ValuationSubring.ofPrime.congr_simpstatement and proof · cited by 1
- ValuationSubring.idealOfLE_ofPrimestatement and proof · cited by 0
- ValuationSubring.ofPrime_le_of_lestatement and proof · cited by 0
- ValuationSubring.ofPrime_valuation_eq_one_iff_mem_primeComplstatement and proof · cited by 0