mathlib documentation

data.nat.factorization.prime_pow

Prime powers and factorizations #

This file deals with factorizations of prime powers.

theorem is_prime_pow_iff_unique_prime_dvd {n : } :
is_prime_pow n ∃! (p : ), nat.prime p p n

An equivalent definition for prime powers: n is a prime power iff there is a unique prime dividing it.

theorem is_prime_pow_pow_iff {n k : } (hk : k 0) :
theorem nat.coprime.is_prime_pow_dvd_mul {n a b : } (hab : a.coprime b) (hn : is_prime_pow n) :
n a * b n a n b