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
Victor Tsynkov (Jun 20 2020 at 20:04):
@Johan Commelin Thanks. With your input, I see that I can get it from
But a more general variant for arbitrary powers is still not obvious.
Johan Commelin (Jun 20 2020 at 20:07):
nat.coprime.pow doesn't exist, then you can write it. It's 3 lines if you use
Yury G. Kudryashov (Jun 20 2020 at 20:51):
It should be
Mario Carneiro (Jun 20 2020 at 22:30):
I'm pretty sure this exists
Mario Carneiro (Jun 20 2020 at 22:31):
Mario Carneiro (Jun 20 2020 at 22:32):
pow_pow is actually just called
Last updated: May 07 2021 at 19:12 UTC