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
Instances for is_prime_pow
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 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) :
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 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]
Equations
theorem is_prime_pow.dvd {n m : } (hn : is_prime_pow n) (hm : m n) (hm₁ : m 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) :
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 is_prime_pow.two_le {n : } :
is_prime_pow n2 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