div by p_adic_val_nat is coprime

Stream: Is there code for X?

[Chris Birkbeck]

Do we have :

lemma p_val_nat_div_coprime (a p : ℕ) (ha :  0 < a ) (hp:  0 < p):
  coprime p (a/ p^(padic_val_nat p a)) :=

(Maybe this needs prime p, but I think the padic_val_nat should work fine in this case).

[Yaël Dillies]

It doesn't need prime. Instead it needs squarefree.

[Yaël Dillies]

Trouble happens when padic_val_nat is the "true valuation", but rounded down. For example 2 / 4 ^ padic_val_nat 4 2 is 2, not 1.

[Stuart Presnell]

I've just PRed (#14576) a version of this for factorization, which uses an assumption of prime p.

[Chris Birkbeck]

Yaël Dillies said:

Trouble happens when padic_val_nat is the "true valuation", but rounded down. For example 2 / 4 ^ padic_val_nat 4 2 is 2, not 1.

ah good point! tbh all I need is the prime case

[Chris Birkbeck]

Stuart Presnell said:

I've just PRed (#14576) a version of this for factorization, which uses an assumption of prime p.

Great!

[Stuart Presnell]

Yaël Dillies said:

It doesn't need prime. Instead it needs squarefree.

Coming back to this: squarefree isn't the relevant criterion, what's needed is coprime p n. For example, when n = 21 and p = 15 we have padic_val_nat p n = 0 and so coprime p (n / p ^ (padic_val_nat p n)) is false.

So, using the generalised pow_padic_val_nat_dvd I've PRed in #14637, we have

example {n p : ℕ} (hpn : p.coprime n) :
  coprime p (n / p ^ (padic_val_nat p n)) :=
coprime.coprime_div_right hpn (pow_padic_val_nat_dvd p n)

[Yaël Dillies]

But... coprime p n means that padic_val_nat p n = 0, so you're just restating coprime p n in a complicated way.

[Stuart Presnell]

Oh, of course

[Stuart Presnell]

So how does squarefree help here?

[Yaël Dillies]

It helps if you assume p ∣ n on top.

[Yaël Dillies]

Well, actually no it doesn't really seem to help.

[Mario Carneiro]

A quick unit test suggests that \forall a > 0, coprime p (a/ p^(padic_val_nat p a)) is true exactly when prime p or p = 1

[Mario Carneiro]

the p = 1 case is boring since everything is coprime to 1

[Mario Carneiro]

The counterexample is: if p = a * b where a, b > 1, then padic_val_nat p a = 0 so a / p^(padic_val_nat p a) = a but gcd p a = a != 1

[Stuart Presnell]

So that suggests that there's no further interesting generalisation beyond coprime_of_div_pow_factorization in #14576.

[Chris Birkbeck]

The prime case is the only one I need so I'm happy with that

[Stuart Presnell]

Chris Birkbeck said:

The prime case is the only one I need so I'm happy with that

#14576 is merged now, so docs#nat.coprime_of_div_pow_factorization should be available

[Chris Birkbeck]

Great, thank you!