mathlib3 documentation


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]