How to prove dvd_of_pow_dvd_pow?

Stream: Is there code for X?

[Casavaca]

How can I prove this?

theorem dvd_of_pow_dvd_pow {α : Type*} [CommMonoid α] {a b : α} {n : ℕ} (hn : 0 < n) (h : a ^ n ∣ b ^ n) : a ∣ b := by sorry

theorem Int.dvd_of_pow_dvd_pow {a b : ℤ} {n : ℕ} (hn : 0 < n)
  (h : a ^ n ∣ b ^ n) : a ∣ b := by sorry

[Damiano Testa]

I'm not sure your first lemma is true: does it work for Z/p^3, a=p^2, b=p, n=3?

[Casavaca]

You are right. I'll update my message.

[Damiano Testa]

import Mathlib.Data.Int.GCD

theorem Int.dvd_of_pow_dvd_pow {a b : ℤ} {n : ℕ} (hn : 0 < n)
    (h : a ^ n ∣ b ^ n) : a ∣ b := by
  exact? says exact (pow_dvd_pow_iff hn).mp h

[Riccardo Brasca]

Strangely enough I also missed to find this very recently. I am adding in #11767 a generalization (and also changing the assumption to n \neq 0)

[Riccardo Brasca]

I've thought a little bit about it, and I don't think one can do better than integrally closed domains (being a domain is not enough)

[Casavaca]

Thank you. Now I know why I missed it and what I should do:

I missed it because I just imported Mathlib.Tactics and use moogle to search for tactics. I found some tactic but not applicable in my case.
I should just import the whole Mathlib and try exact? or apply?

[Damiano Testa]

(I found the import by running exact? using import Mathlib and then reduced the import to the one containing the lemma.)

[Yury G. Kudryashov]

I found docs#Nat.pow_dvd_pow_iff and docs#Int.pow_dvd_pow_iff in loogle.

[Riccardo Brasca]

We now have IsIntegrallyClosed.pow_dvd_pow_iff that I thought was general enough for basically any purpose. But then I realized that in flt-regular we need it for Ideal R (here R is a Dedekind domain), and the problem is that Ideal R is only a semiring, IsIntegrallyClosed.pow_dvd_pow_iff does not apply. On the other hand, the results holds because Ideal R is a unique factorization monoid (the proof it's not hard).

Does anyone see a generalization that cover these two cases? (The theory of integrally closed semirings looks scary :D)

[Kevin Buzzard]

Interesting question! I just read the proof in the integrally closed domain case and the nontrivial direction goes like this: if b^n = x * a^n then working in the field of fractions we see that b/a is integral because its n'th power is x, so b/a is in the ground ring.

Is it really such a sin to just prove the result again for unique factorisation monoids? UFDs are integrally closed but the concept doesn't make sense for monoids. We surely have lemmas which are true for commrings but also true for Nat and we just reprove for Nat. We also have lemmas which are true for groups and for groups with 0 and again we just state them twice rather than trying to find a common generalisation eg 'groups which might have a zero".

[Yaël Dillies]

Kevin Buzzard said:

We also have lemmas which are true for groups and for groups with 0 and again we just state them twice rather than trying to find a common generalisation eg 'groups which might have a zero".

docs#DivisionMonoid :sweat:

[Kevin Buzzard]

Ok so we _sometimes_ just state them twice :-)

[Riccardo Brasca]

Of course we can have it twice, I was just wondering if there is a reasonable generalization (I think the standard mathlib solution for important things when there is no common generalization is to define a new class where the result holds by definition, but this is surely an overkill here).

[Yakov Pechersky]

Does docs#DecompositionMonoid or docs#WfDvdMonoid help?

[Riccardo Brasca]

I don't think so: we already have a proof of

lemma pow_dvd_pow_iff_dvd {M : Type*} [CancelCommMonoidWithZero M] [UniqueFactorizationMonoid M]
    {a b : M} {x : ℕ} (h' : x ≠ 0) : a ^ x ∣ b ^ x ↔ a ∣ b

but the thing is that if R is a ring, assuming UniqueFactorizationMonoid R is not necessary (it holds with [IsDomain R] [IsIntegrallyClosed R], that is weaker) and I don't see a common generalization.

[Kevin Buzzard]

WfDvd is too strong because things like the integers in C_p satisfy this (they're integrally closed but not a UFD). But what about decomposition monoids which are domains? Is the result true for those? This covers the integers of C_p, and ideals in a Dedekind domain.