Theorems · Definition · commutative algebra

HomogeneousLocalization.NumDenSameDeg.embedding

{ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          (𝒜 : ι → σ) → (x : Submonoid A) → HomogeneousLocalization.NumDenSameDeg 𝒜 x → Localization x

For x : prime ideal of A and any p : NumDenSameDeg 𝒜 x, or equivalent a numerator and a denominator of the same degree, we get an element p.num / p.den of Aₓ.

Defined in

Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization

Cited by

9 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext

Assumes

CommRingSetLike