English
If r and r' are associated, then IsLocalization.Away r S holds if and only if IsLocalization.Away r' S, since they define the same localization away from R.
Русский
Если r и r' ассоциированы, то IsLocalization.Away r S верно тогда и только тогда, когда IsLocalization.Away r' S, поскольку они задают одну и ту же локализацию away.
LaTeX
$$$\\text{Associated}(r,r') \\Rightarrow IsLocalization.Away\\; r\\; S \\iff IsLocalization.Away\\; r'\\; S$$$
Lean4
/-- If `r` and `r'` are associated elements of `R`, an `R`-algebra `S`
is the localization of `R` away from `r` if and only of it is the localization of `R` away from
`r'`. -/
theorem iff_of_associated {r r' : R} (h : Associated r r') : IsLocalization.Away r S ↔ IsLocalization.Away r' S :=
⟨fun _ ↦ IsLocalization.Away.of_associated h, fun _ ↦ IsLocalization.Away.of_associated h.symm⟩
