Theorems · Theorem · commutative algebra

gcd_greatest_associated

∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b d : α},
  d ∣ a → d ∣ b → (∀ (e : α), e ∣ a → e ∣ b → e ∣ d) → Associated d (gcd a b)

Defined in

Mathlib.Algebra.GCDMonoid.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroGCDMonoid