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