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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• UniqueFactorizationMonoid.toNormalizedGCDMonoid α = NormalizedGCDMonoid.mk ⋯ ⋯

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