Is there a theorem `pow_eq_pow_iff_of_coprime` for Nat?

Stream: Is there code for X?

[Lingwei Peng (彭灵伟)]

Hi all,

I’m looking for a theorem on natural numbers that states:

If m and n are coprime, then

a^m = b^n if and only if there exists some c such that a = c^n and b = c^m.

I was trying to state it as:

import Mathlib

theorem pow_eq_pow_iff_of_coprime' {a b m n : ℕ} (h1 : m.Coprime n) : a^m = b^n ↔ ∃ c, a = c^n ∧ b = c^m := by
  sorry

[Riccardo Brasca]

You can probably get there via docs#pow_eq_pow_iff_of_coprime, that is close (but it doesn't work for ℕ). Let me see.

[Lingwei Peng (彭灵伟)]

Yes, I found that it doesn’t work for Nat too.

[Riccardo Brasca]

I don't have time right now, but here is a start

import Mathlib

theorem pow_eq_pow_iff_of_coprime' {a b m n : ℕ} (h1 : m.Coprime n) : a^m = b^n ↔ ∃ c, a = c^n ∧ b = c^m := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · replace h : (a : ℚ) ^ m = b ^ n := by norm_cast
    obtain ⟨c, hca, hcb⟩ := (pow_eq_pow_iff_of_coprime h1).mp h
    sorry
  · obtain ⟨c, rfl, rfl⟩ := h
    ring

[Riccardo Brasca]

I would finish showing that c is the coercion of a natural number. This follows from something like docs#irrational_nrt_of_notint_nrt, but for rational numbers.

[Riccardo Brasca]

This holds for example since Z is integrally closed, but it is more elementary.

[Riccardo Brasca]

This

import Mathlib

open Polynomial FaithfulSMul

variable {R : Type*} [CommRing R] [IsIntegrallyClosed R] [IsDomain R]

theorem IsIntegrallyClosed.pow_eq_pow_iff_of_coprime (a b : R) {m n : ℕ} (hnm : m.Coprime n) :
    a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m := by
  let K := FractionRing R
  refine ⟨fun h ↦ ?_, fun ⟨c, hac, hbc⟩ ↦ by simp [hac, hbc, ← pow_mul, mul_comm]⟩
  by_cases hn : n = 0
  · simp_all
  apply_fun (algebraMap R K) at h
  obtain ⟨c, hca, hcb⟩ := (_root_.pow_eq_pow_iff_of_coprime hnm).mp (by simpa [map_pow] using h)
  rsuffices ⟨d, rfl⟩ : ∃ d, algebraMap R K d = c
  · exact ⟨d, algebraMap_injective R K (by simp [hca]), algebraMap_injective R K (by simp [hcb])⟩
  exact algebraMap_eq_of_integral ⟨X ^ n - C a, monic_X_pow_sub_C a hn, by simp [hca]⟩

works for ℤ. It shouldn't be too hard to get to the Nat version.

[Ruben Van de Velde]

That seems very heavy handed. Does the approach with Nat.gcdA/B not work directly?

[Riccardo Brasca]

I've not tried, but as I said the result for ℕ and ℤ is actually completely elementary.

[Jz Pan]

Why IsIntegrallyClosed is coming? Does it have counterexamples for $\Z[\sqrt{-3}]$?

[Riccardo Brasca]

I don't have any specific counterexample, but what is possible is that, for a domain R with field of fraction K, there is an element x in K but not in R such that x^n is in R.

[Riccardo Brasca]

What happens in the proof is pretty clear, you want to use Bezout on the exponents, so you need to take negative powers, in particular you need to work in the field of fractions. I haven't thought if this is really necessary.

[Andrew Yang]

In $\mathbb{Z}[\sqrt{8}]$, $8$ is both a square and a cube but not a 6-th power of anything.

[Riccardo Brasca]

Anyway we surely want the above version. Feel free to PR it.

[Lingwei Peng (彭灵伟)]

Thanks，I got the Nat version based on your answer.