prime powers

Stream: new members

[Scott Morrison]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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