English
If r and r' are associated elements of R, then the localization of R away from r S is equivalent to the localization away from r' S: IsLocalization.Away r S ↔ IsLocalization.Away r' S.
Русский
Если элементы r и r' в R являются ассоциированными, то локализация R away от r эквивалентна локализации away от r': IsLocalization.Away r S ↔ IsLocalization.Away r' S.
LaTeX
$$$\\text{Associated}(r,r') \\Rightarrow (IsLocalization.Away\\; r\\; S \\iff IsLocalization.Away\\; r'\\; S)$$$
Lean4
theorem of_associated {r r' : R} (h : Associated r r') [IsLocalization.Away r S] : IsLocalization.Away r' S :=
by
obtain ⟨u, rfl⟩ := h
refine mk _ ?_ (fun s ↦ ?_) (fun a b hab ↦ ?_)
· simp [algebraMap_isUnit r, IsUnit.map _ u.isUnit]
· obtain ⟨n, a, hn⟩ := surj r s
use n, a * u ^ n
simp [mul_pow, ← mul_assoc, hn]
· obtain ⟨n, hn⟩ := exists_of_eq r hab
use n
rw [mul_pow, mul_comm (r ^ n), mul_assoc, mul_assoc, hn]
