radical_onehundredtwenty
plain-language theorem explainer
The radical of 120 equals 30. Number theorists checking small composite cases in arithmetic functions would cite this when confirming the square-free kernel for 120. The proof is a one-line native decision that evaluates the radical definition directly on the prime factors 2, 3, and 5.
Claim. $rad(120) = 30$, where $rad(n)$ is the product of the distinct prime factors of the natural number $n$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function as a foothold for later Dirichlet inversion. The radical extracts the square-free kernel of an integer. Upstream result states: The radical of n is the product of its distinct prime factors, implemented as the product over the primeFactors set.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the radical definition on input 120.
why it matters
This concrete instance supports validation inside the arithmetic functions module, which prepares Möbius and related tools. It fills a specific case in the number theory primitives without yet feeding parent theorems. The module doc notes that deeper algebra can be layered once basic interfaces stabilize.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.