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.

Equations
    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] [NoZeroDivisors R] :
      ¬IsPrimePow 0
      source
      theorem IsPrimePow.not_unit {R : Type u_1} [CommMonoidWithZero R] {n : R} (h : IsPrimePow n) :
      ¬IsUnit n
      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] [NoZeroDivisors 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 instDecidableIsPrimePowNat {n : ℕ} :
      Decidable (IsPrimePow n)
      Equations
        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