# Zulip Chat Archive

## 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