mathlib3 documentation

algebra.is_prime_pow

Prime powers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
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
source
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
source
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).

source
theorem not_is_prime_pow_zero {R : Type u_1} [comm_monoid_with_zero R] [no_zero_divisors R] :
¬is_prime_pow 0
source
theorem is_prime_pow.not_unit {R : Type u_1} [comm_monoid_with_zero R] {n : R} (h : is_prime_pow n) :
¬is_unit n
source
theorem is_unit.not_is_prime_pow {R : Type u_1} [comm_monoid_with_zero R] {n : R} (h : is_unit n) :
¬is_prime_pow n
source
theorem not_is_prime_pow_one {R : Type u_1} [comm_monoid_with_zero R] :
¬is_prime_pow 1
source
theorem prime.is_prime_pow {R : Type u_1} [comm_monoid_with_zero R] {p : R} (hp : prime p) :
is_prime_pow p
source
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)
source
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
source
theorem is_prime_pow.ne_one {R : Type u_1} [comm_monoid_with_zero R] {n : R} (h : is_prime_pow n) :
n ≠ 1
source
theorem is_prime_pow_nat_iff (n : ℕ) :
is_prime_pow n ↔ ∃ (p k : ℕ), nat.prime p ∧ 0 < k ∧ p ^ k = n
source
theorem nat.prime.is_prime_pow {p : ℕ} (hp : nat.prime p) :
is_prime_pow p
source
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
source
@[protected, instance]
def is_prime_pow.decidable {n : ℕ} :
decidable (is_prime_pow n)
Equations
source
theorem is_prime_pow.dvd {n m : ℕ} (hn : is_prime_pow n) (hm : m ∣ n) (hm₁ : m ≠ 1) :
is_prime_pow m
source
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)
source
theorem is_prime_pow.two_le {n : ℕ} :
is_prime_pow n → 2 ≤ n
source
theorem is_prime_pow.pos {n : ℕ} (hn : is_prime_pow n) :
0 < n
source
theorem is_prime_pow.one_lt {n : ℕ} (h : is_prime_pow n) :
1 < n