Theorems · Definition · commutative algebra

HomogeneousLocalization.AtPrime

{ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} → [inst : CommRing A] → [SetLike σ A] → (ι → σ) → (𝔭 : Ideal A) → [𝔭.IsPrime] → Type (max u_1 u_2)

Localizing a ring homogeneously at a prime ideal.

Defined in

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Cited by

36 results in Mathlib

Foundations

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

Assumes

CommRingSetLikeIdeal.IsPrime