Theorems · Definition · commutative algebra

strongNormalizedGCDMonoidOfExistsGCD

{α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] →
      [StrongNormalizationMonoid α] →
        [DecidableEq α] → (∀ (a b : α), ∃ c, ∀ (d : α), d ∣ a ∧ d ∣ b ↔ d ∣ c) → StrongNormalizedGCDMonoid α

Define a StrongNormalizedGCDMonoid structure on a monoid just from the existence of a gcd.

Defined in

Mathlib.Algebra.GCDMonoid.Basic

Cited by

1 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidWithZeroIsCancelMulZeroStrongNormalizationMonoidDecidableEq