# GCD domains are integrally closed #

source
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
source
@[instance 100]
instance GCDMonoid.toIsIntegrallyClosed {R : Type u_1} [CommRing R] [IsDomain R] [h : Nonempty (GCDMonoid R)] :
IsIntegrallyClosed R