## 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: May 07 2021 at 19:12 UTC