Documentation

Mathlib.Algebra.IsPrimePow

Prime powers #

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

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

Instances For
    source
    theorem isPrimePow_def {R : Type u_1} [CommMonoidWithZero R] (n : R) :
    IsPrimePow n ↔ ∃ (p : R), ∃ (k : ℕ), Prime p ∧ 0 < k ∧ p ^ k = n
    source
    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).

    source
    theorem not_isPrimePow_zero {R : Type u_1} [CommMonoidWithZero R] [IsReduced R] :
    ¬IsPrimePow 0
    source
    theorem IsPrimePow.not_isUnit {R : Type u_1} [CommMonoidWithZero R] {n : R} (h : IsPrimePow n) :
    ¬IsUnit n
    source
    @[deprecated IsPrimePow.not_isUnit (since := "2026-08-02")]
    theorem IsPrimePow.not_unit {R : Type u_1} [CommMonoidWithZero R] {n : R} (h : IsPrimePow n) :
    ¬IsUnit n

    Alias of IsPrimePow.not_isUnit.

    source
    theorem IsUnit.not_isPrimePow {R : Type u_1} [CommMonoidWithZero R] {n : R} (h : IsUnit n) :
    ¬IsPrimePow n
    source
    theorem not_isPrimePow_one {R : Type u_1} [CommMonoidWithZero R] :
    ¬IsPrimePow 1
    source
    theorem Prime.isPrimePow {R : Type u_1} [CommMonoidWithZero R] {p : R} (hp : Prime p) :
    IsPrimePow p
    source
    theorem IsPrimePow.pow {R : Type u_1} [CommMonoidWithZero R] {n : R} (hn : IsPrimePow n) {k : ℕ} (hk : k ≠ 0) :
    IsPrimePow (n ^ k)
    source
    theorem IsPrimePow.ne_zero {R : Type u_1} [CommMonoidWithZero R] [IsReduced R] {n : R} (h : IsPrimePow n) :
    n ≠ 0
    source
    theorem IsPrimePow.ne_one {R : Type u_1} [CommMonoidWithZero R] {n : R} (h : IsPrimePow n) :
    n ≠ 1
    source
    theorem isPrimePow_nat_iff (n : ℕ) :
    IsPrimePow n ↔ ∃ (p : ℕ), ∃ (k : ℕ), Nat.Prime p ∧ 0 < k ∧ p ^ k = n
    source
    theorem Nat.Prime.isPrimePow {p : ℕ} (hp : Prime p) :
    IsPrimePow p
    source
    theorem isPrimePow_nat_iff_bounded (n : ℕ) :
    IsPrimePow n ↔ ∃ (p : ℕ), p ≤ n ∧ ∃ (k : ℕ), k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n
    source
    theorem isPrimePow_nat_iff_bounded_log (n : ℕ) :
    IsPrimePow n ↔ ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ (p : ℕ), p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
    source
    theorem isPrimePow_nat_iff_bounded_log_minFac (n : ℕ) :
    IsPrimePow n ↔ ∃ (k : ℕ), k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k
    source
    @[instance_reducible]
    instance instDecidableIsPrimePowNat {n : ℕ} :
    Decidable (IsPrimePow n)
    source
    theorem IsPrimePow.dvd {n m : ℕ} (hn : IsPrimePow n) (hm : m ∣ n) (hm₁ : m ≠ 1) :
    IsPrimePow m
    source
    theorem IsPrimePow.two_le {n : ℕ} :
    IsPrimePow n → 2 ≤ n
    source
    theorem IsPrimePow.pos {n : ℕ} (hn : IsPrimePow n) :
    0 < n
    source
    theorem IsPrimePow.one_lt {n : ℕ} (h : IsPrimePow n) :
    1 < n