radical_one_eq
plain-language theorem explainer
radical(1) equals 1 follows directly from the definition of the radical as the product of distinct prime factors. Number theorists working with arithmetic functions in the Recognition Science layer would cite this identity as the base case for multiplicative calculations and square-free decompositions. The proof is a one-line wrapper that applies native_decide to evaluate the definition at n=1.
Claim. $rad(1)=1$, where $rad(n)$ denotes the product of the distinct prime factors of the positive integer $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related objects such as the radical. The radical is defined directly as the product of the distinct prime factors of n via n.primeFactors.prod id. This supplies the value at the unit element under that definition.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the definition of radical at 1.
why it matters
This identity anchors the arithmetic functions module and supplies the n=1 case required for consistent multiplicative properties. It supports later Möbius and square-free results in the Recognition Science number theory layer, though no downstream theorems are recorded yet. The result closes the base case for radical computations without invoking deeper forcing chain steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.