Building GCD out of unique factorization

Main results

• UniqueFactorizationMonoid.toGCDMonoid: choose a GCD monoid structure given unique factorization.

noncomputable def UniqueFactorizationMonoid.toGCDMonoid (α : Type u_2) [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] : GCDMonoid α

toGCDMonoid constructs a GCD monoid out of a unique factorization domain.

noncomputable def UniqueFactorizationMonoid.toNormalizedGCDMonoid (α : Type u_2) [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] [NormalizationMonoid α] : NormalizedGCDMonoid α

toNormalizedGCDMonoid constructs a GCD monoid out of a normalization on a unique factorization domain.

instance instNonemptyNormalizedGCDMonoidOfUniqueFactorizationMonoid (α : Type u_2) [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] : Nonempty (NormalizedGCDMonoid α)