Zulip Chat Archive

Stream: new members

Topic: gcd over naturals is positive


Rick Love (Aug 15 2020 at 16:07):

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

Shing Tak Lam (Aug 15 2020 at 16:09):

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 (Aug 15 2020 at 16:10):

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

Rick Love (Aug 15 2020 at 16:11):

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 (Aug 15 2020 at 16:15):

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 (Aug 15 2020 at 16:26):

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 (Aug 15 2020 at 16:27):

But gcd 1 1 = 1 is coprime

Alex J. Best (Aug 15 2020 at 17:06):

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 (Aug 15 2020 at 17:11):

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


Last updated: Dec 20 2023 at 11:08 UTC