mathlib documentation


Prime powers and factorizations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file deals with factorizations of prime powers.

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