Theorems · Definition · commutative algebra

normalizedGCDMonoidOfLCM

{α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] →
      [inst_2 : NormalizationMonoid α] →
        [DecidableEq α] →
          (lcm : α → α → α) →
            (∀ (a b : α), a ∣ lcm a b) →
              (∀ (a b : α), b ∣ lcm a b) →
                (∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a) →
                  (∀ (a b : α), normalize (lcm a b) = lcm a b) → NormalizedGCDMonoid α

Define NormalizedGCDMonoid on a structure just from the lcm and its properties.

Defined in

Mathlib.Algebra.GCDMonoid.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroIsCancelMulZeroNormalizationMonoidDecidableEq