Converse of nat.coprime_pow

Stream: new members

[Lars Ericson]

We have

theorem coprime.pow {k l : ℕ} (m n : ℕ) (H1 : coprime k l) : coprime (k ^ m) (l ^ n)

Is there a converse available in mathlib? Something like

import data.num.prime
import tactic
import tactic.slim_check

lemma coprime_power_N (a p n : ℕ)
 (hp: num.prime p) (ha: a > 0) (hac: a.coprime (p ^ n)) :
  a.coprime p :=
by slim_check

[Sebastien Gouezel]

You have docs#nat.coprime.coprime_mul_left_right

[Sebastien Gouezel]

The statement as you wrote it is wrong, though. Can you see why?

[Kevin Buzzard]

Sebastien is probably referring to the maths error but there's also the issue that you probably want nat.prime

[Lars Ericson]

My logic is this: I'm assuming that a>0 and a and p^n have no positive integer factors in common other than 1. p^n is prime so it's only prime factor is p. a has a factorization a=q1^n1 * q2^n2 ...qm^nm where none of the qi = p. This means that a is coprime with p assuming that it is coprime with p^n.

So there is something wrong with that logic, but I don't see it. I'm not actively trying to be obtuse, I just don't see the flaw in that logic, which is what I'm trying to translate to Lean.

[Kevin Buzzard]

p^n isn't prime in general, and p might not be a prime factor of p^n.

[Lars Ericson]

I am assuming that p is a prime natural number. By the fundamental theorem of arithmetic, every positive integer has a unique prime factorization. For me, the prime factorization of x=p^n is the list of pairs [(p,n)], and x=p^n. To say that p is a prime factor of x is just to say that it is a member of that list. I don't understand what you mean by prime factorization. Clearly p is in the list of prime factors of x=p^n. So I don't understand what you mean by p is not a prime factor of p^n.

To give another example to describe my notion of prime factorization, if had a number y = p^3 * q ^4 * r^2, where p, q and r are prime, then the prime factorization of y would be the list [(p,3), (q,4), (r,2)].

The context here is natural numbers, not some other kind of number. In particular 2^n where n is a natural number, but I was trying to generalize a little to p^n where p is a prime natural number and n is a natural number.

[Kevin Buzzard]

As is so often the case in mathematics, your mistake is in the sentence which starts "Clearly".

[Paul van Wamelen]

Sure, p is a factor of p^n, but not for all n...

[Lars Ericson]

Thank you @Sebastien Gouezel @Kevin Buzzard and @Paul van Wamelen for your kind assistance. With your help, the following is close enough to what I was trying to prove and it checks:

import data.num.prime

lemma coprime_power_N (a p n : ℕ)
                      (hp: nat.prime p)
                      (ha: a > 0)
                      (hn: n > 0)
                      (hac: a.coprime (p ^ n)) :
                      a.coprime p :=
begin
  induction n with d hd,
  exfalso,
  exact nat.lt_asymm hn hn,
  rw (nat.succ_eq_add_one d) at hac,
  rw (pow_succ' p d) at hac,
  exact (nat.coprime.coprime_mul_left_right hac),
end