GCD domains are integrally closed #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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]