isPrimePow_nat_iff — Mathlib

English

For natural numbers, IsPrimePow n is equivalent to the existence of a prime p and k > 0 with p^k = n.

Русский

Для натуральных IsPrimePow n эквивалентно существованию простого p и k > 0 с p^k = n.

LaTeX

$$$\text{IsPrimePow } n \;\leftrightarrow\; \exists p\in\mathbb{N}, \exists k\in\mathbb{N}, \text{Nat.Prime } p \land 0 < k \land p^k = n$$$

Lean4

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

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