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 : IsPrimePow n) :
n.minFac ^ n.factorization n.minFac = n
theorem isPrimePow_of_minFac_pow_factorization_eq {n : } (h : n.minFac ^ n.factorization n.minFac = n) (hn : n 1) :
theorem isPrimePow_iff_minFac_pow_factorization_eq {n : } (hn : n 1) :
IsPrimePow n n.minFac ^ n.factorization n.minFac = n
theorem isPrimePow_iff_factorization_eq_single {n : } :
IsPrimePow n ∃ (p : ) (k : ), 0 < k n.factorization = Finsupp.single p k
theorem isPrimePow_iff_card_primeFactors_eq_one {n : } :
IsPrimePow n n.primeFactors.card = 1
theorem IsPrimePow.exists_ord_compl_eq_one {n : } (h : IsPrimePow n) :
∃ (p : ), p.Prime n / p ^ n.factorization p = 1
theorem exists_ord_compl_eq_one_iff_isPrimePow {n : } (hn : n 1) :
IsPrimePow n ∃ (p : ), p.Prime n / p ^ n.factorization p = 1
theorem isPrimePow_iff_unique_prime_dvd {n : } :
IsPrimePow n ∃! p : , p.Prime 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 : a.Coprime b) (hn : IsPrimePow n) :
n a * b n a n b
theorem Nat.mul_divisors_filter_prime_pow {a : } {b : } (hab : a.Coprime b) :
Finset.filter IsPrimePow (a * b).divisors = Finset.filter IsPrimePow (a.divisors b.divisors)