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