instNonemptyNormalizedGCDMonoidOfUniqueFactorizationMonoid

English

There exists a normalized gcd monoid structure associated to any UniqueFactorizationMonoid, giving a canonical gcd framework.

Русский

Для любой уникализированной факторизационной моноиды существует структура нормализованного gcd-моноида.

LaTeX

$$$\\text{Nonempty}(\\text{NormalizedGCDMonoid } \\alpha)$$$

Lean4

instance (α) [CancelCommMonoidWithZero α] [UniqueFactorizationMonoid α] : Nonempty (NormalizedGCDMonoid α) :=
  by
  letI := UniqueFactorizationMonoid.normalizationMonoid (α := α)
  classical exact ⟨UniqueFactorizationMonoid.toNormalizedGCDMonoid α⟩

Похожие утверждения