Mathlib.Algebra.IsPrimePow

IsPrimePow definition

: Prop

Full source

/-- `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`. -/
def IsPrimePow : Prop :=
  ∃ (p : R) (k : ℕ), Prime p ∧ 0 < k ∧ p ^ k = n

Prime power

Informal description

A natural number $ n $ is a prime power if there exists a prime number $ p $ and a positive integer $ k $ such that $ n = p^k $.

isPrimePow_def theorem

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

Full source

theorem isPrimePow_def : IsPrimePowIsPrimePow n ↔ ∃ (p : R) (k : ℕ), Prime p ∧ 0 < k ∧ p ^ k = n :=
  Iff.rfl

Characterization of Prime Powers: $n$ is a prime power $\iff$ $\exists p$ prime, $k > 0$ such that $n = p^k$

Informal description

A natural number $n$ is a prime power if and only if there exists a prime number $p$ and a positive integer $k$ such that $n = p^k$.

isPrimePow_iff_pow_succ theorem

: IsPrimePow n ↔ ∃ (p : R) (k : ℕ), Prime p ∧ p ^ (k + 1) = n

Full source

/-- 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_iff_pow_succ : IsPrimePowIsPrimePow n ↔ ∃ (p : R) (k : ℕ), Prime p ∧ p ^ (k + 1) = n :=
  (isPrimePow_def _).trans
    ⟨fun ⟨p, k, hp, hk, hn⟩ => ⟨p, k - 1, hp, by rwa [Nat.sub_add_cancel hk]⟩, fun ⟨_, _, hp, hn⟩ =>
      ⟨_, _, hp, Nat.succ_pos', hn⟩⟩

Characterization of Prime Powers via Successor Exponent: $n$ is a prime power $\iff$ $\exists p$ prime, $k \in \mathbb{N}$ such that $n = p^{k+1}$

Informal description

A natural number $n$ is a prime power if and only if there exists a prime number $p$ and a natural number $k$ such that $n = p^{k+1}$.

not_isPrimePow_zero theorem

[NoZeroDivisors R] : ¬IsPrimePow (0 : R)

Full source

theorem not_isPrimePow_zero [NoZeroDivisors R] : ¬IsPrimePow (0 : R) := by
  simp only [isPrimePow_def, not_exists, not_and', and_imp]
  intro x n _hn hx
  rw [pow_eq_zero hx]
  simp

Zero is not a prime power in a semiring without zero divisors

Informal description

In a commutative semiring $R$ with no zero divisors, the zero element $0$ is not a prime power.

IsPrimePow.not_unit theorem

{n : R} (h : IsPrimePow n) : ¬IsUnit n

Full source

theorem IsPrimePow.not_unit {n : R} (h : IsPrimePow n) : ¬IsUnit n :=
  let ⟨_p, _k, hp, hk, hn⟩ := h
  hn ▸ (isUnit_pow_iff hk.ne').not.mpr hp.not_unit

Prime powers are not units

Informal description

For any element $n$ in a commutative monoid $R$, if $n$ is a prime power (i.e., $n = p^k$ for some prime $p$ and positive integer $k$), then $n$ is not a unit in $R$.

IsUnit.not_isPrimePow theorem

{n : R} (h : IsUnit n) : ¬IsPrimePow n

Full source

theorem IsUnit.not_isPrimePow {n : R} (h : IsUnit n) : ¬IsPrimePow n := fun h' => h'.not_unit h

Units Are Not Prime Powers

Informal description

For any element $n$ in a commutative monoid $R$, if $n$ is a unit, then $n$ is not a prime power.

not_isPrimePow_one theorem

: ¬IsPrimePow (1 : R)

Full source

theorem not_isPrimePow_one : ¬IsPrimePow (1 : R) :=
  isUnit_one.not_isPrimePow

One is Not a Prime Power

Informal description

The multiplicative identity element $1$ in a commutative monoid $R$ is not a prime power.

Prime.isPrimePow theorem

{p : R} (hp : Prime p) : IsPrimePow p

Full source

theorem Prime.isPrimePow {p : R} (hp : Prime p) : IsPrimePow p :=
  ⟨p, 1, hp, zero_lt_one, by simp⟩

Primes are Prime Powers

Informal description

For any prime element $p$ in a commutative monoid $R$, $p$ is a prime power.

IsPrimePow.pow theorem

{n : R} (hn : IsPrimePow n) {k : ℕ} (hk : k ≠ 0) : IsPrimePow (n ^ k)

Full source

theorem IsPrimePow.pow {n : R} (hn : IsPrimePow n) {k : ℕ} (hk : k ≠ 0) : IsPrimePow (n ^ k) :=
  let ⟨p, k', hp, hk', hn⟩ := hn
  ⟨p, k * k', hp, mul_pos hk.bot_lt hk', by rw [pow_mul', hn]⟩

Prime Powers are Closed under Nonzero Exponentiation

Informal description

For any element $n$ in a commutative monoid $R$, if $n$ is a prime power and $k$ is a nonzero natural number, then $n^k$ is also a prime power.

IsPrimePow.ne_zero theorem

[NoZeroDivisors R] {n : R} (h : IsPrimePow n) : n ≠ 0

Full source

theorem IsPrimePow.ne_zero [NoZeroDivisors R] {n : R} (h : IsPrimePow n) : n ≠ 0 := fun t =>
  not_isPrimePow_zero (t ▸ h)

Nonzero Property of Prime Powers in Semirings Without Zero Divisors

Informal description

In a commutative semiring $R$ with no zero divisors, if an element $n$ is a prime power, then $n$ is not equal to zero.

IsPrimePow.ne_one theorem

{n : R} (h : IsPrimePow n) : n ≠ 1

Full source

theorem IsPrimePow.ne_one {n : R} (h : IsPrimePow n) : n ≠ 1 := fun t =>
  not_isPrimePow_one (t ▸ h)

Prime powers are not equal to one

Informal description

For any element $n$ in a commutative monoid $R$, if $n$ is a prime power, then $n$ is not equal to the multiplicative identity $1$.

isPrimePow_nat_iff theorem

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

Full source

theorem isPrimePow_nat_iff (n : ℕ) : IsPrimePowIsPrimePow n ↔ ∃ p k : ℕ, Nat.Prime p ∧ 0 < k ∧ p ^ k = n := by
  simp only [isPrimePow_def, Nat.prime_iff]

Characterization of Prime Powers in Natural Numbers

Informal description

A natural number $n$ is a prime power if and only if there exists a prime number $p$ and a positive integer $k$ such that $n = p^k$.

Nat.Prime.isPrimePow theorem

{p : ℕ} (hp : p.Prime) : IsPrimePow p

Full source

theorem Nat.Prime.isPrimePow {p : ℕ} (hp : p.Prime) : IsPrimePow p :=
  _root_.Prime.isPrimePow (prime_iff.mp hp)

Primes are Prime Powers in Natural Numbers

Informal description

For any prime natural number $p$, there exists a positive integer $k$ such that $p = p^k$, i.e., $p$ is a prime power.

isPrimePow_nat_iff_bounded theorem

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

Full source

theorem isPrimePow_nat_iff_bounded (n : ℕ) :
    IsPrimePowIsPrimePow n ↔ ∃ p : ℕ, p ≤ n ∧ ∃ k : ℕ, k ≤ n ∧ p.Prime ∧ 0 < k ∧ p ^ k = n := by
  rw [isPrimePow_nat_iff]
  refine Iff.symm ⟨fun ⟨p, _, k, _, hp, hk, hn⟩ => ⟨p, k, hp, hk, hn⟩, ?_⟩
  rintro ⟨p, k, hp, hk, rfl⟩
  refine ⟨p, ?_, k, (Nat.lt_pow_self hp.one_lt).le, hp, hk, rfl⟩
  conv => { lhs; rw [← (pow_one p)] }
  exact Nat.pow_le_pow_right hp.one_lt.le hk

Bounded Characterization of Prime Powers: $n$ is a prime power iff $\exists p \leq n, \exists k \leq n, \text{prime } p \land k > 0 \land n = p^k$

Informal description

A natural number $n$ is a prime power if and only if there exists a prime number $p \leq n$ and a positive integer $k \leq n$ such that $n = p^k$.

instDecidableIsPrimePowNat instance

{n : ℕ} : Decidable (IsPrimePow n)

Full source

instance {n : ℕ} : Decidable (IsPrimePow n) :=
  decidable_of_iff' _ (isPrimePow_nat_iff_bounded n)

Decidability of Prime Powers for Natural Numbers

Informal description

For any natural number $n$, the property of being a prime power is decidable. That is, there exists an algorithm to determine whether $n$ can be written as $p^k$ for some prime $p$ and positive integer $k$.

IsPrimePow.dvd theorem

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

Full source

theorem IsPrimePow.dvd {n m : ℕ} (hn : IsPrimePow n) (hm : m ∣ n) (hm₁ : m ≠ 1) : IsPrimePow m := by
  rw [isPrimePow_nat_iff] at hn ⊢
  rcases hn with ⟨p, k, hp, _hk, rfl⟩
  obtain ⟨i, hik, rfl⟩ := (Nat.dvd_prime_pow hp).1 hm
  refine ⟨p, i, hp, ?_, rfl⟩
  apply Nat.pos_of_ne_zero
  rintro rfl
  simp only [pow_zero, ne_eq, not_true_eq_false] at hm₁

Divisibility Preserves Prime Power Property

Informal description

Let $n$ and $m$ be natural numbers such that $n$ is a prime power, $m$ divides $n$, and $m \neq 1$. Then $m$ is also a prime power.

IsPrimePow.two_le theorem

: ∀ {n : ℕ}, IsPrimePow n → 2 ≤ n

Full source

theorem IsPrimePow.two_le : ∀ {n : ℕ}, IsPrimePow n → 2 ≤ n
  | 0, h => (not_isPrimePow_zero h).elim
  | 1, h => (not_isPrimePow_one h).elim
  | _n + 2, _ => le_add_self

Prime Powers are at Least Two

Informal description

For any natural number $n$, if $n$ is a prime power, then $2 \leq n$.

IsPrimePow.pos theorem

{n : ℕ} (hn : IsPrimePow n) : 0 < n

Full source

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

Positivity of Prime Powers

Informal description

For any natural number $n$, if $n$ is a prime power, then $n$ is positive, i.e., $0 < n$.

IsPrimePow.one_lt theorem

{n : ℕ} (h : IsPrimePow n) : 1 < n

Full source

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

Prime Powers are Greater Than One

Informal description

For any natural number $n$, if $n$ is a prime power, then $1 < n$.