/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public meta import Mathlib.Algebra.GCDMonoid.Finset
public meta import Mathlib.Algebra.GCDMonoid.Nat
public meta import Mathlib.Data.Nat.Factorization.Defs
import Mathlib.Tactic@[expose] public sectionnamespace NatA 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.
def IsPerfectPower (n : ℕ) : Prop :=
∃ k m : ℕ, 1 < k ∧ 1 < m ∧ k ^ m = nn:ℕhn:n > 1g:ℕ := n.primeFactors.gcd ⇑n.factorizationhgcd:g > 1hg_def:g = n.primeFactors.gcd ⇑n.factorizationf:ℕ → ℕ := fun q ↦ q ^ (n.factorization q / g)k:ℕ := n.primeFactors.prod fhk_def:k = n.primeFactors.prod fh_eq:k ^ g = ∏ q ∈ n.primeFactors, q ^ (n.factorization q / g * g)hn_ne_zero:n ≠ 0p:ℕhp:p ∉ n.primeFactorshp_not_in_support:p ∉ n.factorization.support⊢ p ^ (n.factorization p / g * g) = (fun x1 x2 ↦ x1 ^ x2) p (n.factorization p)
n:ℕhn:n > 1g:ℕ := n.primeFactors.gcd ⇑n.factorizationhgcd:g > 1hg_def:g = n.primeFactors.gcd ⇑n.factorizationf:ℕ → ℕ := fun q ↦ q ^ (n.factorization q / g)k:ℕ := n.primeFactors.prod fhk_def:k = n.primeFactors.prod fh_eq:k ^ g = ∏ q ∈ n.primeFactors, q ^ (n.factorization q / g * g)hn_ne_zero:n ≠ 0p:ℕhp:p ∉ n.primeFactorshp_not_in_support:p ∉ n.factorization.supporthp_zero:n.factorization p = 0⊢ p ^ (n.factorization p / g * g) = (fun x1 x2 ↦ x1 ^ x2) p (n.factorization p)
All goals completed! 🐙instance IsPerfectPower.decide : ∀ n, Decidable (IsPerfectPower n) := fun n =>
decidable_of_iff (n > 1 ∧ n.primeFactors.gcd n.factorization > 1)
(isPerfectPower_iff_factorization_gcd n).symmexample : IsPerfectPower 4 := ⊢ IsPerfectPower 4 All goals completed! 🐙example : IsPerfectPower 27 := ⊢ IsPerfectPower 27 All goals completed! 🐙example : ¬IsPerfectPower 0 := ⊢ ¬IsPerfectPower 0 All goals completed! 🐙example : ¬IsPerfectPower 1 := ⊢ ¬IsPerfectPower 1 All goals completed! 🐙example : ¬IsPerfectPower 2 := ⊢ ¬IsPerfectPower 2 All goals completed! 🐙end Nat