Building GCD out of unique factorization

Main results

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

@[implicit_reducible]

noncomputable def UniqueFactorizationMonoid.toGCDMonoid (α : Type u_2) [CommMonoidWithZero α] [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.

@[implicit_reducible]

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

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

Equations

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

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