English
The localization away from a unit is isomorphic to the original ring: there is an algebra isomorphism R ≃_R S when x is a unit and S is the localization away from x.
Русский
Локализация away от единицы из кольца изоморфна самому кольцу: существует алгебраическое изоморфие R ≃_R S, когда x — единица и S — локализация away от x.
LaTeX
$$$\\exists \\text{AlgIso}_{R}(R,S) \\text{ with } \\text{isUnit}(x) \\Rightarrow IsLocalization.Away x S \\simeq R$$$
Lean4
/-- The localization away from a unit is isomorphic to the ring. -/
noncomputable def atUnit (x : R) (e : IsUnit x) [IsLocalization.Away x S] : R ≃ₐ[R] S :=
atUnits R (Submonoid.powers x) (by rwa [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff])
