Localization of a UFD

Main results

• UniqueFactorizationMonoid.localization : The localization of a UFD is still a UFD.

theorem UniqueFactorizationMonoid.of_isLocalization {R : Type u_1} [CommRing R] [UniqueFactorizationMonoid R] [IsDomain R] (M : Submonoid R) (S : Type u_2) [CommRing S] [Algebra R S] [IsLocalization M S] : UniqueFactorizationMonoid S

If S is the localization of a UFD R, then S is also a UFD.

instance UniqueFactorizationMonoid.localization {R : Type u_1} [CommRing R] [UniqueFactorizationMonoid R] [IsDomain R] (M : Submonoid R) : UniqueFactorizationMonoid (Localization M)

The localization of a UFD is still a UFD.