mathlib documentation

algebra.is_prime_pow

Prime powers #

This file deals with prime powers: numbers which are positive integer powers of a single prime.

def is_prime_pow {R : Type u_1} [comm_monoid_with_zero R] (n : R) :

Prop

n is a prime power if there is a prime p and a positive natural k such that n can be written as p^k.

Equations

is_prime_pow n = ∃ (p : R) (k : ℕ), prime p ∧ 0 < k ∧ p ^ k = n

theorem is_prime_pow_def {R : Type u_1} [comm_monoid_with_zero R] (n : R) :

is_prime_pow n ↔ ∃ (p : R) (k : ℕ), prime p ∧ 0 < k ∧ p ^ k = n

theorem is_prime_pow_iff_pow_succ {R : Type u_1} [comm_monoid_with_zero R] (n : R) :

is_prime_pow n ↔ ∃ (p : R) (k : ℕ), prime p ∧ p ^ (k + 1) = n

An equivalent definition for prime powers: n is a prime power iff there is a prime p and a natural k such that n can be written as p^(k+1).

theorem not_is_prime_pow_zero {R : Type u_1} [comm_monoid_with_zero R] [no_zero_divisors R] :

¬is_prime_pow 0

theorem not_is_prime_pow_one {R : Type u_1} [comm_monoid_with_zero R] :

¬is_prime_pow 1

theorem prime.is_prime_pow {R : Type u_1} [comm_monoid_with_zero R] {p : R} (hp : prime p) :

theorem is_prime_pow.pow {R : Type u_1} [comm_monoid_with_zero R] {n : R} (hn : is_prime_pow n) {k : ℕ} (hk : k ≠ 0) :

is_prime_pow (n ^ k)

theorem is_prime_pow.ne_zero {R : Type u_1} [comm_monoid_with_zero R] [no_zero_divisors R] {n : R} (h : is_prime_pow n) :

n ≠ 0

theorem is_prime_pow.ne_one {R : Type u_1} [comm_monoid_with_zero R] {n : R} (h : is_prime_pow n) :

n ≠ 1

theorem eq_of_prime_pow_eq {R : Type u_1} [cancel_comm_monoid_with_zero R] [unique Rˣ] {p₁ p₂ : R} {k₁ k₂ : ℕ} (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₁ : 0 < k₁) (h : p₁ ^ k₁ = p₂ ^ k₂) :

p₁ = p₂

theorem eq_of_prime_pow_eq' {R : Type u_1} [cancel_comm_monoid_with_zero R] [unique Rˣ] {p₁ p₂ : R} {k₁ k₂ : ℕ} (hp₁ : prime p₁) (hp₂ : prime p₂) (hk₁ : 0 < k₂) (h : p₁ ^ k₁ = p₂ ^ k₂) :

p₁ = p₂

theorem is_prime_pow_nat_iff (n : ℕ) :

is_prime_pow n ↔ ∃ (p k : ℕ), nat.prime p ∧ 0 < k ∧ p ^ k = n

theorem nat.prime.is_prime_pow {p : ℕ} (hp : nat.prime p) :

theorem is_prime_pow_nat_iff_bounded (n : ℕ) :

is_prime_pow n ↔ ∃ (p : ℕ), p ≤ n ∧ ∃ (k : ℕ), k ≤ n ∧ nat.prime p ∧ 0 < k ∧ p ^ k = n

@[protected, instance]

def is_prime_pow.decidable {n : ℕ} :

decidable (is_prime_pow n)

Equations

is_prime_pow.decidable = decidable_of_iff' (∃ (p : ℕ), p ≤ n ∧ ∃ (k : ℕ), k ≤ n ∧ nat.prime p ∧ 0 < k ∧ p ^ k = n) _

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.dvd {n m : ℕ} (hn : is_prime_pow n) (hm : m ∣ n) (hm₁ : m ≠ 1) :

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_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.disjoint_divisors_filter_prime_pow {a b : ℕ} (hab : a.coprime b) :

disjoint (finset.filter is_prime_pow a.divisors) (finset.filter is_prime_pow b.divisors)

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)

theorem is_prime_pow.two_le {n : ℕ} :

is_prime_pow n → 2 ≤ n

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

0 < n

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

1 < n