Documentation

Mathlib.RingTheory.Localization.Away.AdjoinRoot

The R-AlgEquiv between the localization of R away from r and R with an inverse of r adjoined.

source
noncomputable def Localization.awayEquivAdjoin {R : Type u_1} [CommRing R] (r : R) :
Away r ≃ₐ[R] AdjoinRoot (Polynomial.C r * Polynomial.X - 1)

The R-AlgEquiv between the localization of R away from r and R with an inverse of r adjoined.

Equations
    Instances For
      source
      theorem IsLocalization.adjoin_inv {R : Type u_1} [CommRing R] (r : R) :
      Away r (AdjoinRoot (Polynomial.C r * Polynomial.X - 1))
      source
      theorem IsLocalization.Away.finitePresentation {R : Type u_1} [CommRing R] (r : R) {S : Type u_2} [CommRing S] [Algebra R S] [Away r S] :
      Algebra.FinitePresentation R S