Theorems · Definition · commutative algebra

gcdMonoidOfGCD

{α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] →
      [DecidableEq α] →
        (gcd : α → α → α) →
          (∀ (a b : α), gcd a b ∣ a) →
            (∀ (a b : α), gcd a b ∣ b) → (∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b) → GCDMonoid α

Define GCDMonoid on a structure just from the gcd 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