Documentation

Mathlib.Algebra.IsPrimePow

Prime powers #

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

def IsPrimePow {R : Type u_1} [inst : ] (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
theorem isPrimePow_def {R : Type u_1} [inst : ] (n : R) :
p k, 0 < k p ^ k = n
theorem isPrimePow_iff_pow_succ {R : Type u_1} [inst : ] (n : R) :
p 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} [inst : ] [inst : ] :
theorem IsPrimePow.not_unit {R : Type u_1} [inst : ] {n : R} (h : ) :
theorem IsUnit.not_isPrimePow {R : Type u_1} [inst : ] {n : R} (h : ) :
theorem not_isPrimePow_one {R : Type u_1} [inst : ] :
theorem Prime.isPrimePow {R : Type u_1} [inst : ] {p : R} (hp : ) :
theorem IsPrimePow.pow {R : Type u_1} [inst : ] {n : R} (hn : ) {k : } (hk : k 0) :
theorem IsPrimePow.ne_zero {R : Type u_1} [inst : ] [inst : ] {n : R} (h : ) :
n 0
theorem IsPrimePow.ne_one {R : Type u_1} [inst : ] {n : R} (h : ) :
n 1
theorem isPrimePow_nat_iff (n : ) :
p k, 0 < k p ^ k = n
theorem Nat.Prime.isPrimePow {p : } (hp : ) :
theorem isPrimePow_nat_iff_bounded (n : ) :
p, p n k, k n 0 < k p ^ k = n
Equations
• One or more equations did not get rendered due to their size.
theorem IsPrimePow.dvd {n : } {m : } (hn : ) (hm : m n) (hm₁ : m 1) :
theorem Nat.disjoint_divisors_filter_isPrimePow {a : } {b : } (hab : ) :
Disjoint (Finset.filter IsPrimePow ()) (Finset.filter IsPrimePow ())
theorem IsPrimePow.two_le {n : } :
2 n
theorem IsPrimePow.pos {n : } (hn : ) :
0 < n
theorem IsPrimePow.one_lt {n : } (h : ) :
1 < n