Definition·D055
Greatest common divisor
The common divisor of two numbers that every common divisor divides.
For
not both
(with
the naturals), the greatest common divisor
is the natural number
characterised by
that is,
is a common divisor of
and
that every common divisor divides.
In words
The greatest common divisor of two numbers, not both zero, is a common divisor of them that every common divisor divides: the largest in the sense of divisibility.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Remarks
Existence and uniqueness make the phrase 'the' gcd legitimate. Existence, with the recursion that computes it, is T19. Uniqueness: if
and
both satisfy the characterisation then
and
. Since
are not both
, say
; then
and
each divide the nonzero
, hence are themselves nonzero (were
, then
would give
). So L19 (vii) applies to give
and
, and antisymmetry of the order (L16 forbids both
and
) forces
. This divisibility characterisation is stronger than merely 'numerically largest common divisor', though the two coincide; it is the form that powers Euclid's lemma and unique factorisation. When
the numbers
and
are called coprime.