Theorems · Definition · commutative algebra

IsLocalization.AtPrime

{R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Type u_2) → [inst_1 : CommSemiring S] → [Algebra R S] → (P : Ideal R) → [hp : P.IsPrime] → Prop

Given a prime ideal P, the typeclass IsLocalization.AtPrime S P states that S is isomorphic to the localization of R at the complement of P.

Defined in

Mathlib.RingTheory.Localization.AtPrime.Basic

Cited by

79 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraIdeal.IsPrime