equal prime powers

Stream: Is there code for X?

[Anupam Nayak]

lemma eq_of_eq_prime_pow (p p' : ℕ) (hp : nat.prime p) (hp' : nat.prime p')
(n n' : ℕ+) (h : p ^ (n : ℕ) = p' ^ (n': ℕ)) : p = p' :=

is this in mathlib?

[Yakov Pechersky]

It'd probably be under the injectivity of pow, given that the exponent is positive. Probably uses a hypothesis and not coerced pnats.

[Yakov Pechersky]

You need docs#nat.pow_left_injective and docs#nat.pow_right_injective

[Alex J. Best]

You do need to assume prime, as the exponents are different, right? I don't see this exact lemma in mathlib, but hopefully there is enough things about (unique) factorization that the proof shouldn't be too hard!

[Anupam Nayak]

Yakov Pechersky said:

You need docs#nat.pow_left_injective and docs#nat.pow_right_injective

I am using pow_right_injective to prove n=n' after I have p=p', but i dont see how to prove p=p'

[Yakov Pechersky]

I misread initally and thought some of the bases or exponents were the same.

[Alex J. Best]

Here is a proof:

import data.pnat.factors
open pnat
open nat
lemma eq_of_eq_prime_pow (p p' : ℕ) (hp : nat.prime p) (hp' : nat.prime p')
(n n' : ℕ+) (h : p ^ (n : ℕ) = p' ^ (n': ℕ)) : p = p' :=
begin
  contrapose h,
  intro hpp,
  have : p ∣ p^(↑n) := dvd_pow_self _ (ne_zero n),
  rw hpp at this,
  have hop : p ∣ p' := prime.dvd_of_dvd_pow hp this,
  have : p' ∣ p'^(↑n') := dvd_pow_self _ (ne_zero n'),
  rw ← hpp at this,
  have hop' : p' ∣ p := prime.dvd_of_dvd_pow hp' this,
  apply h,
  exact dvd_antisymm hop hop',
end

[Anupam Nayak]

Alex J. Best said:

Here is a proof:

import data.pnat.factors
open pnat
open nat
lemma eq_of_eq_prime_pow (p p' : ℕ) (hp : nat.prime p) (hp' : nat.prime p')
(n n' : ℕ+) (h : p ^ (n : ℕ) = p' ^ (n': ℕ)) : p = p' :=
begin
  contrapose h,
  intro hpp,
  have : p ∣ p^(↑n) := dvd_pow_self _ (ne_zero n),
  rw hpp at this,
  have hop : p ∣ p' := prime.dvd_of_dvd_pow hp this,
  have : p' ∣ p'^(↑n') := dvd_pow_self _ (ne_zero n'),
  rw ← hpp at this,
  have hop' : p' ∣ p := prime.dvd_of_dvd_pow hp' this,
  apply h,
  exact dvd_antisymm hop hop',
end

Thanks!

[Yury G. Kudryashov]

Another proof:

import data.nat.prime
import data.pnat.basic

open nat

lemma list.head_repeat {α : Type*} [inhabited α] {n : ℕ} (hn : n ≠ 0) (a : α) :
  (list.repeat a n).head = a :=
by { cases n, exacts [(hn rfl).elim, rfl] }

lemma eq_of_eq_prime_pow (p p' : ℕ) (hp : nat.prime p) (hp' : nat.prime p')
  (n n' : ℕ+) (h : p ^ (n : ℕ) = p' ^ (n': ℕ)) : p = p' :=
begin
  apply_fun (list.head ∘ factors) at h,
  simpa [prime.factors_pow, hp, hp', list.head_repeat] using h
end

[Yury G. Kudryashov]

BTW, why nat.factors returns a list, not a multiset?

[Johan Commelin]

I think it's sorted. Which might occasionally be useful, I guess.

[Joanna Choules]

Another proof:

import data.pnat.basic
import data.nat.prime
open pnat
open nat
lemma eq_of_eq_prime_pow (p p' : ℕ) (hp : nat.prime p) (hp' : nat.prime p')
(n n' : ℕ+) (h : p ^ (n : ℕ) = p' ^ (n': ℕ)) : p = p' := begin
  by_contra hne,
  have := coprime_pow_primes n n' hp hp' hne,
  rw [h, coprime_self, pow_eq_one_iff (ne_zero n')] at this,
  exact prime.ne_one hp' this,

  exact nat.linear_order,
  exact ordered_comm_monoid.to_covariant_class_left ℕ,
end

but I'm not sure I understand the necessity of both of the final exacts. Isn't linear_order ℕ, for one, a core fact?

[Yury G. Kudryashov]

Sometimes rw fails to find an instance because the expression is only partially applied (don't know the details). You can close these goals by apply_instance.

[Yury G. Kudryashov]

@Johan Commelin We have docs#multiset.sort

[Yury G. Kudryashov]

But you can't write a @[simp] lemma for factors_pow without extra assumptions unless factors n : multiset nat or finset n : multiset primes.

[Eric Rodriguez]

Yury G. Kudryashov said:

BTW, why nat.factors returns a list, not a multiset?

There's a pnat multiset somewhere, I think as docs#prime_multiset. Pain in the ass to use though.

[Yury G. Kudryashov]

Why do we need a special type for multiset primes?

[Yury G. Kudryashov]

This way we can't apply simp lemmas about multiset.

[Alex J. Best]

Eric Rodriguez said:

Yury G. Kudryashov said:

BTW, why nat.factors returns a list, not a multiset?

There's a pnat multiset somewhere, I think as docs#prime_multiset. Pain in the ass to use though.

I spent 5 mins trying to get that to work for this problem, but it was too annoying trying to coerce everything into pnat.

[Yaël Dillies]

I said somewhere that these pnat files were currently useless because poorly integrated. We should refactor it all.