English
If an algebra S is simultaneously the localization of R at M and at N, then for any R-algebra P, IsLocalization M P holds if and only if IsLocalization N P holds.
Русский
Если алгебра S одновременно является локализацией R по M и по N, то для любой R-алгебры P справедливо: IsLocalization M P эквивалентно IsLocalization N P.
LaTeX
$$$[\text{IsLocalization } M S] \;[\text{IsLocalization } N S] \;[\text{Algebra } R P] \Rightarrow\ (\operatorname{IsLocalization} M P \iff \operatorname{IsLocalization} N P)$$$
Lean4
/-- If an algebra is simultaneously localizations for two submonoids, then an arbitrary algebra
is a localization of one submonoid iff it is a localization of the other. -/
theorem isLocalization_iff_of_isLocalization [IsLocalization M S] [IsLocalization N S] [Algebra R P] :
IsLocalization M P ↔ IsLocalization N P :=
⟨fun _ ↦ isLocalization_of_algEquiv N (algEquiv M S P), fun _ ↦ isLocalization_of_algEquiv M (algEquiv N S P)⟩
