Definition of the greatest common divisor

[benjub]

Currently, https://us.metamath.org/mpeuni/df-gcd.html reads

|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )

There are three unnatural or inelegant things about it:

• it correctly requires that n be smaller than x and y for the divisibility relation, but it demands that it be the greatest such for the <-relation, and not for the divisibility relation,
• it involves RR (that one can simply be replaced by NN0),
• it distinguishes a special case.

All three things are removed with the definition

|- gcd = ( x e. ZZ , y e. ZZ |-> sup ( { n e. NN0 | ( n || x /\ n || y ) } , NN0 , || ) )

I think this is actually more standard than the current one.

Same with df-lcm.

[jkingdon]

What about https://us.metamath.org/mpeuni/dfgcd3.html , (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) ? That's what we use in the iset.mm proof of https://us.metamath.org/ileuni/bezout.html and I think it is what @digama0 thought of as the natural definition of gcd back in some old github comments (not that I went back and re-read them).

Having said that, I don't have an especially strong opinion about what is the definition and what is proved in terms of it, as long as we show they are equivalent.

[avekens]

I agree with @benjub that the current definition is not very comprehensible - unfortunately, there is no justification for it written in the comment (or elsewhere?). It would be good to use a definition from literature, or at least inspired by it, so we can add a bibliographic reference.

For me, both suggestions (from @benjub and @jkingdon ) are fine, but @benjub's version is more intuitively comprehensible, because it explicitly contains the notion of "greatest".

[benjub]

For me, both suggestions (from @benjub and @jkingdon ) are fine, but @benjub's version is more intuitively comprehensible, because it explicitly contains the notion of "greatest".

Indeed. I think that https://us.metamath.org/mpeuni/dfgcd3.html (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) is rather a characterization of the gcd, but is not close enough to the English phrase "greatest common divisor": no explicit notion of "greatest" as you write, nor explicit transcription of "common divisor" (one has to argue that, taking $z$ to be $d$, since $d$ divides itself, then $d$ divides $M$ and $N$, but this is already an argument). Granted, in the standard definition, you first have to show that the sup is actually a greatest element, but this still feels more direct, and in dfgcd3 you have to prove unique existence of the iota.