Zulip Chat Archive

Stream: Is there code for X?

Topic: Results on gcd


Victor Tsynkov (Jun 20 2020 at 19:49):

Not sure if this thread if for such questions: is there anywhere in mathlib a proof of something like this example below? If not, what is the easiest way to get this? I tried library_search with no success. Or am I missing some obvious fact here?

example (n m : ) (h : nat.gcd n m = 1) : nat.gcd (n ^ 2) m = 1 :=
begin
    sorry,
end

Johan Commelin (Jun 20 2020 at 19:52):

I don't know by heart, but I guess this is a lemma about nat.coprime

Victor Tsynkov (Jun 20 2020 at 20:04):

@Johan Commelin Thanks. With your input, I see that I can get it from nat.coprime.mul.
But a more general variant for arbitrary powers is still not obvious.

Johan Commelin (Jun 20 2020 at 20:07):

If nat.coprime.pow doesn't exist, then you can write it. It's 3 lines if you use nat.coprime.mul.

Yury G. Kudryashov (Jun 20 2020 at 20:51):

It should be nat.coprime.pow_left, pow_right, and pow_pow.

Mario Carneiro (Jun 20 2020 at 22:30):

I'm pretty sure this exists

Mario Carneiro (Jun 20 2020 at 22:31):

nat.coprime.pow_left, exactly

Mario Carneiro (Jun 20 2020 at 22:32):

pow_pow is actually just called nat.coprime.pow


Last updated: Dec 20 2023 at 11:08 UTC