Documentation

Mathlib.Algebra.GCDMonoid.IntegrallyClosed

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]
Equations
  • =