English
For a localization map f away from x, there is a canonical multiplicative equivalence between the Away localization at x and N.
Русский
Для локализационной карты fAway от x существует каноническое мультипликативное эквивалентное отображение между локализацией Away от x и N.
LaTeX
$$$ Localization.Away.mulEquivOfQuotient f : Away x \simeq^* N $$$
Lean4
/-- Given `x : M` and a Localization map `f : M →* N` away from `x`, we get an isomorphism between
the Localization of `M` at the Submonoid generated by `x` as a quotient type and `N`. -/
@[to_additive /-- Given `x : M` and a Localization map `f : M →+ N` away from `x`, we get an isomorphism between
the Localization of `M` at the Submonoid generated by `x` as a quotient type and `N`. -/
]
noncomputable def mulEquivOfQuotient (f : Submonoid.LocalizationMap.AwayMap x N) : Away x ≃* N :=
Localization.mulEquivOfQuotient f
