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)
:

Localization.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.

## Instances For

theorem
IsLocalization.adjoin_inv
{R : Type u_1}
[CommRing R]
(r : R)
:

IsLocalization.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]
[IsLocalization.Away r S]
: