mathlib3 documentation

data.nat.factorization.prime_pow

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.

theorem is_prime_pow.min_fac_pow_factorization_eq {n : ℕ} (hn : is_prime_pow n) :

n.min_fac ^ ⇑(n.factorization) n.min_fac = n

theorem is_prime_pow_of_min_fac_pow_factorization_eq {n : ℕ} (h : n.min_fac ^ ⇑(n.factorization) n.min_fac = n) (hn : n ≠ 1) :

theorem is_prime_pow_iff_min_fac_pow_factorization_eq {n : ℕ} (hn : n ≠ 1) :

is_prime_pow n ↔ n.min_fac ^ ⇑(n.factorization) n.min_fac = n

theorem is_prime_pow_iff_factorization_eq_single {n : ℕ} :

is_prime_pow n ↔ ∃ (p k : ℕ), 0 < k ∧ n.factorization = finsupp.single p k

theorem is_prime_pow_iff_card_support_factorization_eq_one {n : ℕ} :

is_prime_pow n ↔ n.factorization.support.card = 1

theorem is_prime_pow.exists_ord_compl_eq_one {n : ℕ} (h : is_prime_pow n) :

∃ (p : ℕ), nat.prime p ∧ n / p ^ ⇑(n.factorization) p = 1

theorem exists_ord_compl_eq_one_iff_is_prime_pow {n : ℕ} (hn : n ≠ 1) :

is_prime_pow n ↔ ∃ (p : ℕ), nat.prime p ∧ n / p ^ ⇑(n.factorization) p = 1

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) :

is_prime_pow (n ^ k) ↔ is_prime_pow n

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

theorem nat.mul_divisors_filter_prime_pow {a b : ℕ} (hab : a.coprime b) :

finset.filter is_prime_pow (a * b).divisors = finset.filter is_prime_pow (a.divisors ∪ b.divisors)