# Prime powers #

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

def IsPrimePow {R : Type u_1} (n : R) :

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
theorem isPrimePow_def {R : Type u_1} (n : R) :
∃ (p : R) (k : ), 0 < k p ^ k = n
theorem isPrimePow_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_isPrimePow_zero {R : Type u_1} [] :
theorem IsPrimePow.not_unit {R : Type u_1} {n : R} (h : ) :
theorem IsUnit.not_isPrimePow {R : Type u_1} {n : R} (h : ) :
theorem not_isPrimePow_one {R : Type u_1} :
theorem Prime.isPrimePow {R : Type u_1} {p : R} (hp : ) :
theorem IsPrimePow.pow {R : Type u_1} {n : R} (hn : ) {k : } (hk : k 0) :
theorem IsPrimePow.ne_zero {R : Type u_1} [] {n : R} (h : ) :
n 0
theorem IsPrimePow.ne_one {R : Type u_1} {n : R} (h : ) :
n 1
theorem isPrimePow_nat_iff (n : ) :
∃ (p : ) (k : ), p.Prime 0 < k p ^ k = n
theorem Nat.Prime.isPrimePow {p : } (hp : p.Prime) :
theorem isPrimePow_nat_iff_bounded (n : ) :
pn, kn, p.Prime 0 < k p ^ k = n
Equations
theorem IsPrimePow.dvd {n : } {m : } (hn : ) (hm : m n) (hm₁ : m 1) :
theorem Nat.disjoint_divisors_filter_isPrimePow {a : } {b : } (hab : a.Coprime b) :
Disjoint (Finset.filter IsPrimePow a.divisors) (Finset.filter IsPrimePow b.divisors)
theorem IsPrimePow.two_le {n : } :
2 n
theorem IsPrimePow.pos {n : } (hn : ) :
0 < n
theorem IsPrimePow.one_lt {n : } (h : ) :
1 < n