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 : Nat.Prime p) :
    IsPrimePow p
    source
    theorem isPrimePow_nat_iff_bounded (n : ℕ) :
    IsPrimePow n ↔ ∃ p ≤ n, ∃ k ≤ n, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
    source
    instance instDecidableIsPrimePowNatToCommMonoidWithZeroLinearOrderedCommMonoidWithZero {n : ℕ} :
    Decidable (IsPrimePow n)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem IsPrimePow.dvd {n : ℕ} {m : ℕ} (hn : IsPrimePow n) (hm : m ∣ n) (hm₁ : m ≠ 1) :
    IsPrimePow m
    source
    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))
    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