GCD domains are integrally closed #
theorem
IsLocalization.surj_of_gcd_domain
{R : Type u_1}
{A : Type u_2}
[CommRing R]
[IsDomain R]
[GCDMonoid R]
[CommRing A]
[Algebra R A]
(M : Submonoid R)
[IsLocalization M A]
(z : A)
:
∃ a b, IsUnit (gcd a b) ∧ z * ↑(algebraMap R A) b = ↑(algebraMap R A) a