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 : R) (b : R), IsUnit (gcd a b) ∧ z * (algebraMap R A) b = (algebraMap R A) a

instance GCDMonoid.toIsIntegrallyClosed {R : Type u_1} [CommRing R] [IsDomain R] [GCDMonoid R] : IsIntegrallyClosed R

Equations

• (_ : IsIntegrallyClosed R) = (_ : IsIntegrallyClosed R)