primeFactors_prime
plain-language theorem explainer
A prime natural number p has prime factors consisting solely of the singleton set containing p. Number theorists building arithmetic functions such as Möbius in the Recognition Science setting would cite this when reducing sums or products over prime cases. The proof is a term-mode wrapper that converts the local Prime predicate to Mathlib's Nat.Prime via prime_iff and applies the standard primeFactors result.
Claim. If $p$ is a prime natural number, then the set of prime factors of $p$ equals the singleton set containing $p$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. The local theoretical setting keeps statements minimal to support later Dirichlet algebra and inversion once basic interfaces stabilize. This theorem operates on the Prime predicate imported from the Basic sibling module and relies on Mathlib's Nat.Prime infrastructure.
proof idea
The term proof first applies the prime_iff lemma to obtain Nat.Prime p from the hypothesis, then invokes Nat.Prime.primeFactors directly on that fact.
why it matters
This result anchors the prime case handling required by the Möbius and squarefree siblings in the same module. It supports consistent factorization steps in the broader Recognition Science number theory layer without introducing new hypotheses. No downstream uses are recorded yet, leaving its role as a foundational interface for later arithmetic expansions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.