Theorems · Definition · commutative algebra

normalizedGCDMonoidOfGCD

{α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] →
      [inst_2 : NormalizationMonoid α] →
        [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) →
                  (∀ (a b : α), normalize (gcd a b) = gcd a b) → NormalizedGCDMonoid α

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