Zulip Chat Archive

Stream: new members

Topic: prime powers


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 04 2019 at 04:13):

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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