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

@[instance 100]

instance GCDMonoid.toIsIntegrallyClosed {R : Type u_1} [CommRing R] [IsDomain R] [h : Nonempty (GCDMonoid R)] : IsIntegrallyClosed R

Equations

• ⋯ = ⋯