Documentation

Mathlib.Algebra.IsPrimePow

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) :

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
    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 IsPrimePow.not_unit {R : Type u_1} [CommMonoidWithZero R] {n : R} (h : IsPrimePow n) :
    theorem IsUnit.not_isPrimePow {R : Type u_1} [CommMonoidWithZero R] {n : R} (h : IsUnit n) :
    theorem Prime.isPrimePow {R : Type u_1} [CommMonoidWithZero R] {p : R} (hp : Prime p) :
    theorem IsPrimePow.pow {R : Type u_1} [CommMonoidWithZero R] {n : R} (hn : IsPrimePow n) {k : } (hk : k 0) :
    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 isPrimePow_nat_iff_bounded (n : ) :
    IsPrimePow n pn, kn, Nat.Prime p 0 < k p ^ k = n
    Equations
    theorem IsPrimePow.dvd {n : } {m : } (hn : IsPrimePow n) (hm : m n) (hm₁ : m 1) :
    theorem Nat.disjoint_divisors_filter_isPrimePow {a : } {b : } (hab : a.Coprime b) :
    Disjoint (Finset.filter IsPrimePow a.divisors) (Finset.filter IsPrimePow b.divisors)
    theorem IsPrimePow.two_le {n : } :
    IsPrimePow n2 n
    theorem IsPrimePow.pos {n : } (hn : IsPrimePow n) :
    0 < n
    theorem IsPrimePow.one_lt {n : } (h : IsPrimePow n) :
    1 < n