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