# mathlibdocumentation

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} (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
Instances for is_prime_pow
theorem is_prime_pow_def {R : Type u_1} (n : R) :
∃ (p : R) (k : ), 0 < k p ^ k = n
theorem is_prime_pow_iff_pow_succ {R : Type u_1} (n : R) :
∃ (p : R) (k : ), 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}  :
theorem not_is_prime_pow_one {R : Type u_1}  :
theorem prime.is_prime_pow {R : Type u_1} {p : R} (hp : prime p) :
theorem is_prime_pow.pow {R : Type u_1} {n : R} (hn : is_prime_pow n) {k : } (hk : k 0) :
theorem is_prime_pow.ne_zero {R : Type u_1} {n : R} (h : is_prime_pow n) :
n 0
theorem is_prime_pow.ne_one {R : Type u_1} {n : R} (h : is_prime_pow n) :
n 1
theorem eq_of_prime_pow_eq {R : Type u_1} [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} [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 : ) :
∃ (p k : ), 0 < k p ^ k = n
theorem nat.prime.is_prime_pow {p : } (hp : nat.prime p) :
theorem is_prime_pow_nat_iff_bounded (n : ) :
∃ (p : ), p n ∃ (k : ), k n 0 < k p ^ k = n
@[protected, instance]
Equations
theorem is_prime_pow.dvd {n m : } (hn : is_prime_pow n) (hm : m n) (hm₁ : m 1) :
theorem nat.disjoint_divisors_filter_prime_pow {a b : } (hab : a.coprime b) :
theorem is_prime_pow.two_le {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