isPrimePow_pow_iff — Mathlib

English

Let n,k be natural numbers with k ≠ 0. Then n^k is a prime power if and only if n is a prime power.

Русский

Пусть n,k принадлежат к множеству натуральных чисел и k ≠ 0. Тогда n^k является степенью простого числа тогда и только тогда, когда n является степенью простого числа.

LaTeX

$$$\forall n,k \in \mathbb{N},\ k \neq 0 \Rightarrow \operatorname{IsPrimePow}(n^k) \iff \operatorname{IsPrimePow}(n)$$$

Lean4

theorem isPrimePow_pow_iff {n k : ℕ} (hk : k ≠ 0) : IsPrimePow (n ^ k) ↔ IsPrimePow n :=
  by
  simp only [isPrimePow_iff_unique_prime_dvd]
  apply existsUnique_congr
  simp +contextual [Nat.prime_iff, Prime.dvd_pow_iff_dvd, hk]

Похожие утверждения