radical_pos
plain-language theorem explainer
The theorem shows that the radical of any positive natural number is strictly positive. Number theorists building arithmetic functions or handling prime factorizations would cite it to guarantee non-vanishing products in multiplicative settings. The proof reduces the claim directly to the product definition of radical and invokes the standard positivity of each prime factor.
Claim. For every positive integer $n$, the radical of $n$ satisfies $0 <$ rad$(n)$, where rad$(n)$ is the product of the distinct prime factors of $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and related constructs. The radical is defined as rad$(n) := n$.primeFactors.prod id, the product of distinct primes dividing $n$. This positivity result supplies a basic non-vanishing property needed for square-free checks and further Möbius applications in the file.
proof idea
The term proof first simplifies the goal by unfolding the definition of radical. It then applies Finset.prod_pos, whose hypothesis is discharged by showing that each prime factor p satisfies Nat.Prime.pos (Nat.prime_of_mem_primeFactors hp).
why it matters
The result supplies a foundational positivity property for the radical inside the arithmetic functions module that supports Möbius footholds. It fills a basic lemma slot in the NumberTheory.Primes hierarchy, though the current dependency graph lists no direct downstream users.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.