Prime powers

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

def IsPrimePow {R : Type u_1} [CommMonoidWithZero 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

• IsPrimePow n = ∃ (p : R) (k : ℕ), Prime p ∧ 0 < k ∧ p ^ k = n

theorem isPrimePow_def {R : Type u_1} [CommMonoidWithZero R] (n : R) : IsPrimePow n ↔ ∃ (p : R) (k : ℕ), Prime p ∧ 0 < k ∧ p ^ k = n

theorem isPrimePow_iff_pow_succ {R : Type u_1} [CommMonoidWithZero R] (n : R) : IsPrimePow 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 not_isPrimePow_zero {R : Type u_1} [CommMonoidWithZero R] [NoZeroDivisors R] : ¬IsPrimePow 0

theorem IsPrimePow.not_unit {R : Type u_1} [CommMonoidWithZero R] {n : R} (h : IsPrimePow n) : ¬IsUnit n

theorem IsUnit.not_isPrimePow {R : Type u_1} [CommMonoidWithZero R] {n : R} (h : IsUnit n) : ¬IsPrimePow n

theorem not_isPrimePow_one {R : Type u_1} [CommMonoidWithZero R] : ¬IsPrimePow 1

theorem Prime.isPrimePow {R : Type u_1} [CommMonoidWithZero R] {p : R} (hp : Prime p) : IsPrimePow p

theorem IsPrimePow.pow {R : Type u_1} [CommMonoidWithZero R] {n : R} (hn : IsPrimePow n) {k : ℕ} (hk : k ≠ 0) : IsPrimePow (n ^ k)

theorem IsPrimePow.ne_zero {R : Type u_1} [CommMonoidWithZero R] [NoZeroDivisors R] {n : R} (h : IsPrimePow n) : n ≠ 0

theorem IsPrimePow.ne_one {R : Type u_1} [CommMonoidWithZero R] {n : R} (h : IsPrimePow n) : n ≠ 1

theorem isPrimePow_nat_iff (n : ℕ) : IsPrimePow n ↔ ∃ (p : ℕ) (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n

theorem Nat.Prime.isPrimePow {p : ℕ} (hp : Nat.Prime p) : IsPrimePow p

theorem isPrimePow_nat_iff_bounded (n : ℕ) : IsPrimePow n ↔ ∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

instance instDecidableIsPrimePowNatToCommMonoidWithZeroInstLinearOrderedCommMonoidWithZero {n : ℕ} : Decidable (IsPrimePow n)

Equations

• instDecidableIsPrimePowNatToCommMonoidWithZeroInstLinearOrderedCommMonoidWithZero = decidable_of_iff' (∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ⋯

theorem IsPrimePow.dvd {n : ℕ} {m : ℕ} (hn : IsPrimePow n) (hm : m ∣ n) (hm₁ : m ≠ 1) : IsPrimePow m

theorem Nat.disjoint_divisors_filter_isPrimePow {a : ℕ} {b : ℕ} (hab : Nat.Coprime a b) : Disjoint (Finset.filter IsPrimePow (Nat.divisors a)) (Finset.filter IsPrimePow (Nat.divisors b))

theorem IsPrimePow.two_le {n : ℕ} : IsPrimePow n → 2 ≤ n

theorem IsPrimePow.pos {n : ℕ} (hn : IsPrimePow n) : 0 < n

theorem IsPrimePow.one_lt {n : ℕ} (h : IsPrimePow n) : 1 < n