Theorems · Definition · commutative algebra

normalizedGCDMonoidOfExistsGCD

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

Define a NormalizedGCDMonoid 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 26 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidWithZeroIsCancelMulZeroNormalizationMonoidDecidableEq