# Documentation

Mathlib.Data.Nat.Factorization.PrimePow

# Prime powers and factorizations #

This file deals with factorizations of prime powers.

theorem IsPrimePow.minFac_pow_factorization_eq {n : } (hn : ) :
^ ↑() () = n
theorem isPrimePow_of_minFac_pow_factorization_eq {n : } (h : ^ ↑() () = n) (hn : n 1) :
theorem isPrimePow_iff_minFac_pow_factorization_eq {n : } (hn : n 1) :
^ ↑() () = n
theorem isPrimePow_iff_factorization_eq_single {n : } :
p k, 0 < k = fun₀ | p => k
theorem IsPrimePow.exists_ord_compl_eq_one {n : } (h : ) :
p, n / p ^ ↑() p = 1
theorem exists_ord_compl_eq_one_iff_isPrimePow {n : } (hn : n 1) :
p, n / p ^ ↑() p = 1
theorem isPrimePow_iff_unique_prime_dvd {n : } :
∃! p, p n

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

theorem isPrimePow_pow_iff {n : } {k : } (hk : k 0) :
theorem Nat.Coprime.isPrimePow_dvd_mul {n : } {a : } {b : } (hab : ) (hn : ) :
n a * b n a n b
theorem Nat.mul_divisors_filter_prime_pow {a : } {b : } (hab : ) :
Finset.filter IsPrimePow (Nat.divisors (a * b)) = Finset.filter IsPrimePow ()