radical_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not extend the claim to n = 0 or to non-natural numbers.
- Does not compute explicit values or bounds for the radical beyond positivity.
- Does not address interactions with other arithmetic functions such as Euler totient.
formal statement (Lean)
858theorem radical_pos {n : ℕ} (_hn : 0 < n) : 0 < radical n := by
proof body
Term-mode proof.
859 simp only [radical]
860 exact Finset.prod_pos (fun p hp => Nat.Prime.pos (Nat.prime_of_mem_primeFactors hp))
861
862/-! ### Coprimality power lemmas -/
863
864/-- Coprimality is preserved by powers on the left. -/