isPrimePow_def — Mathlib

English

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

Русский

Число n является степенью простого числа тогда и только тогда, когда существует простое p и положительная степень k, такая что n = p^k.

LaTeX

$$$\text{IsPrimePow } n \;\Longleftrightarrow\; \exists p\;\exists k\; (\text{Prime } p) \land 0 < k \land p^k = n$$$

Lean4

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

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