Theorems · Definition · commutative algebra

strongNormalizedGCDMonoidOfExistsLCM

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

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

Defined in

Mathlib.Algebra.GCDMonoid.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroIsCancelMulZeroStrongNormalizationMonoidDecidableEq