mathlib documentation

algebra.gcd_monoid.integrally_closed

GCD domains are integrally closed #

theorem is_localization.surj_of_gcd_domain {R : Type u_1} {A : Type u_2} [comm_ring R] [is_domain R] [gcd_monoid R] [comm_ring A] [algebra R A] (M : submonoid R) [is_localization M A] (z : A) :
∃ (a b : R), is_unit (gcd_monoid.gcd a b) z * (algebra_map R A) b = (algebra_map R A) a
@[protected, instance]