Theorems · Definition · commutative algebra

normalizedGCDMonoidOfExistsLCM

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

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

Defined in

Mathlib.Algebra.GCDMonoid.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroIsCancelMulZeroNormalizationMonoidDecidableEq