Building GCD out of unique factorization

Main results

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

@[instance_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.

@[instance 100]

instance instIsGCDMonoidOfUniqueFactorizationMonoid (α : Type u_2) [CommMonoidWithZero α] [UniqueFactorizationMonoid α] : IsGCDMonoid α

@[instance_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.

@[reducible, inline]

noncomputable abbrev UniqueFactorizationMonoid.toStrongNormalizedGCDMonoid (α : Type u_2) [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [StrongNormalizationMonoid α] : StrongNormalizedGCDMonoid α

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

Equations

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