radical_le
plain-language theorem explainer
rad(n) ≤ n holds for every positive integer n. Number theorists estimating arithmetic functions via square-free kernels would cite this bound when bounding products over distinct primes. The term-mode proof unfolds the radical definition then applies the standard divisibility of the prime-factor product to obtain the inequality via Nat.le_of_dvd.
Claim. For every natural number $n ≠ 0$, $rad(n) ≤ n$, where $rad(n)$ denotes the product of the distinct prime factors of $n$.
background
The radical of a positive integer n is the square-free kernel obtained as the product of its distinct prime factors. This declaration appears in the arithmetic functions module that supplies lightweight wrappers around Mathlib's library, beginning with the Möbius function for later Dirichlet inversion. It depends directly on the upstream definition radical n := n.primeFactors.prod id.
proof idea
The term proof first simplifies the radical definition, invokes Nat.prod_primeFactors_dvd to record that the product divides n, then applies Nat.le_of_dvd together with Nat.pos_of_ne_zero to conclude the inequality from the positive divisor.
why it matters
This supplies the elementary upper bound on the radical that supports later arithmetic-function arguments in the primes layer. No direct downstream users are recorded yet, but the inequality is a standard prerequisite for estimates involving square-free parts. It fills a basic property in the number-theory scaffolding without touching Recognition Science chain steps T0-T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.