def Nat.IsPerfectPower (n : ℕ) : Prop

A perfect power is a natural number that is a product of equal natural factors, or, in other words, an integer that can be expressed as a square or a higher integer power of another integer greater than one. More formally, $n$ is a perfect power if there exist natural numbers $m > 1$, and $k > 1$ such that $m ^ k = n$. In this case, $n$ may be called a perfect $k$th power. If $k = 2$ or $k = 3$, then $n$ is called a perfect square or perfect cube, respectively.

Equations

• n.IsPerfectPower = ∃ (k : ℕ) (m : ℕ), 1 < k ∧ 1 < m ∧ k ^ m = n

theorem Nat.isPerfectPower_iff_factorization_gcd (n : ℕ) : n.IsPerfectPower ↔ n > 1 ∧ n.primeFactors.gcd ⇑n.factorization > 1

instance Nat.IsPerfectPower.decide (n : ℕ) : Decidable n.IsPerfectPower

Equations

• Nat.IsPerfectPower.decide n = decidable_of_iff (n > 1 ∧ n.primeFactors.gcd ⇑n.factorization > 1) ⋯