primeFactors_prime_pow
plain-language theorem explainer
The theorem asserts that if p is prime and k is a positive integer then the prime factors of p^k form exactly the singleton {p}. Number theorists simplifying radical or Möbius expressions over prime powers cite this when reducing sums or products to single terms. The proof is a one-line wrapper that converts the local Prime predicate to Nat.Prime via the equivalence prime_iff and invokes the Mathlib theorem Nat.primeFactors_prime_pow.
Claim. Let $p$ be a prime number and let $k$ be a positive integer. Then the set of prime factors of $p^k$ equals the singleton set containing $p$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Prime is the transparent alias for Nat.Prime. The equivalence prime_iff states that Prime n holds precisely when Nat.Prime n holds. This result sits inside the arithmetic-functions layer that prepares Möbius inversion and von Mangoldt sums for later use in the Recognition Science number-theory scaffolding.
proof idea
The proof first obtains Nat.Prime p by applying the forward direction of prime_iff to the hypothesis hp. It then passes the nonzero k and the converted prime directly to the Mathlib theorem Nat.primeFactors_prime_pow.
why it matters
The lemma is invoked by radical_prime_pow to conclude that the radical of p^k equals p. It supplies the basic prime-power case needed for the von Mangoldt sum identity and for Möbius inversion over square-free integers. No direct link to the forcing chain or phi-ladder appears here, yet the result closes a small gap in the arithmetic-function interface that the framework relies on for mass formulas and constant derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.