Divisibility of a power by a power of a prime

The multiplicity of a prime p in x ^ n is n times its multiplicity in x (emultiplicity_pow). This file records the resulting divisibility statement: a bound on the power of p dividing x ^ n gives a bound on the power of p dividing x.

Main results

• Prime.pow_succ_dvd_of_pow_mul_add_one_dvd_pow: for a prime p, if p ^ (n * k + 1) divides x ^ n then p ^ (k + 1) divides x.

theorem Prime.pow_succ_dvd_of_pow_mul_add_one_dvd_pow {α : Type u_1} [CommMonoidWithZero α] [IsCancelMulZero α] {p x : α} (hp : Prime p) {n k : ℕ} (h : p ^ (n * k + 1) ∣ x ^ n) : p ^ (k + 1) ∣ x

For a prime p, if p ^ (n * k + 1) divides x ^ n then p ^ (k + 1) divides x: the multiplicity of p in x ^ n is n times that in x.