Theorems · Definition · commutative algebra

gcdMonoidOfLCM

{α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] →
      [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) → GCDMonoid α

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

Defined in

Mathlib.Algebra.GCDMonoid.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroIsCancelMulZeroDecidableEq