radical_one'
plain-language theorem explainer
The radical of a natural number, defined as the product of its distinct prime factors, evaluates to 1 when the input is 1. Number theorists applying arithmetic functions or square-free kernels would cite this identity as the base case for inductive arguments or multiplicative properties. The proof is a direct evaluation that invokes Lean's native decision procedure on the definition.
Claim. $rad(1) = 1$, where $rad(n)$ denotes the product of the distinct prime factors of the natural number $n$.
background
The radical function extracts the square-free kernel of a natural number by multiplying its distinct prime factors. In this module the definition is given directly as the product over the primeFactors set. The surrounding file supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function, and treats radical as a supporting operation for square-free checks.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the equality from the upstream definition of radical.
why it matters
This base case anchors the radical definition inside the arithmetic-functions module that supports Möbius-related identities. It supplies the empty-product convention required for any later multiplicative extension or inversion formula. No downstream use is recorded yet, and the declaration sits outside the Recognition Science forcing chain (T0-T8) or phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.