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

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

• One or more equations did not get rendered due to their size.

theorem IsLocalization.adjoin_inv {R : Type u_1} [CommRing R] (r : R) : Away r (AdjoinRoot (Polynomial.C r * Polynomial.X - 1))

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