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