## Stream: new members

### Topic: prime powers

#### Scott Morrison (Oct 04 2019 at 04:05):

Do we have

lemma prime_pow_dvd_prime_pow {p k l : ℕ} (pp : prime p) : p^k ∣ p^l ↔ k ≤ l := sorry


in mathlib?

#### Scott Morrison (Oct 04 2019 at 04:05):

I can't even find anything about the multiplicity of a prime in the prime factorisation of a number.

#### Johan Commelin (Oct 04 2019 at 04:13):

In the multiplicity file there are statements that look suspiciously close to what you want

#### Johan Commelin (Oct 04 2019 at 04:14):

But I don't think that they make the connection to the prime factorisation of a nat

#### Johan Commelin (Oct 04 2019 at 04:16):

Also, your proposed theorem is true for all p ≥ 2 (don't need prime), so maybe it is called nat.le_of_pow_dvd_pow or something like the (if might be an iff).

#### Floris van Doorn (Oct 04 2019 at 04:25):

I don't think it's quite there. In the multiplicity file it's a combination of pow_dvd_iff_le_multiplicity and multiplicity_pow_self (modulo some casting). group_power has one direction: pow_dvd_pow.

#### Johan Commelin (Oct 04 2019 at 04:30):

We want pow_strict_mono for p > 1 in linearly ordered commutative semirings, I guess

Last updated: May 08 2021 at 18:17 UTC