gcd over naturals is positive

Stream: new members

[Rick Love]

I couldn't find a way to prove that gcd is positive.

[Shing Tak Lam]

Probably because gcd 0 0 = 0. However nat.gcd_pos_of_pos_(left|right) are there if you know that at least one of the inputs is positive.

[Rick Love]

Ok, I found those. I'm figuring out how to apply them.

[Rick Love]

Ok, I figured out how to use them:

theorem gcd_pos (a b : ℕ):
    a > 0 ∨ b > 0 ->
    gcd a b > 0:=
begin
    intro h,
    cases h with p q,
    apply gcd_pos_of_pos_left,
    apply p,

    apply gcd_pos_of_pos_right,
    apply q,
end

[Rick Love]

Also with pos naturals:

theorem gcd_pos_pnat (a b : ℕ+):
    gcd a b > 0:=
begin
    apply gcd_pos_of_pos_left,
    simp,
end

[Rick Love]

This means, that gcd 0 0 = 0 is not coprime with this definition:

@[reducible] def coprime (m n : ℕ) : Prop := gcd m n = 1

[Rick Love]

But gcd 1 1 = 1 is coprime

[Alex J. Best]

That sounds about right, I think gcd 0 0 = 0 is quite standard with whatever definition you take, and likewise 0 not being coprime with itself.

[Kenny Lau]

note that 2 is also not coprime with itself because gcd 2 2 = 2