Theorems · Definition · commutative algebra
Localization.AtPrime
{R : Type u_1} → [inst : CommSemiring R] → (P : Ideal R) → [hp : P.IsPrime] → Type u_1Given a prime ideal P, Localization.AtPrime P is a localization of
R at the complement of P, as a quotient type.
- Cited by
- 299 results in Mathlib
- Foundations
- Depth 31 from the axioms, rests on 350 definitions · uses propext, Quot.sound
- Assumes
- CommSemiringIdeal.IsPrime
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- Idealstatement and proof · cited by 4,748
- Ideal.IsPrimestatement and proof · cited by 827
- Ideal.primeComplproof · cited by 462
- Localizationproof · cited by 270
Cited by364
Results whose statement or proof uses this declaration.
- Ideal.ResidueFieldproof · cited by 119
- Ideal.ramificationIdxproof · cited by 59
- Localization.localRingHomstatement and proof · cited by 54
- Module.rankAtStalkproof · cited by 41
- Algebra.IsUnramifiedAtproof · cited by 35
- Localization.AtPrime.algebraOfLiesOverstatement · cited by 30
- Algebra.QuasiFiniteAtproof · cited by 29
- Localization.AtPrime.IsLiesOverAlgebrastatement · cited by 23
- Ideal.ResidueField.mapₐstatement · cited by 21
- Localization.AtPrime.map_eq_maximalIdealstatement and proof · cited by 17
- MaximalSpectrum.PiLocalizationproof · cited by 17
- Module.freeLocusproof · cited by 15
Showing the 200 most cited of 364.