radical_prime'
plain-language theorem explainer
The radical of a prime p equals p itself. Number theorists handling square-free decompositions or Möbius inversion would cite this identity as a basic reduction step. The proof converts the local Prime hypothesis to Nat.Prime via the equivalence lemma, unfolds the radical definition, and reduces the prime-factors product directly to p by simplification.
Claim. If $p$ is prime then the radical of $p$ equals $p$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function, and defines the radical of $n$ as the product of its distinct prime factors. The local Prime predicate is a transparent alias for Nat.Prime, with the equivalence theorem prime_iff establishing the identification. Upstream results include the radical definition stating that rad(n) is the product of distinct prime factors and the prime_iff equivalence.
proof idea
The term proof first obtains Nat.Prime p from the hypothesis via prime_iff. It then unfolds radical, rewrites with Nat.Prime.primeFactors to obtain the singleton set, and finishes by simplification.
why it matters
This identity supplies a basic reduction for arithmetic-function identities in the module, including those involving the Möbius function on square-free inputs. It forms part of the number-theoretic scaffolding in the Recognition Science monolith, though no downstream uses are recorded. It supports clean handling of primes ahead of any Dirichlet or inversion arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.