radical_six'
plain-language theorem explainer
The radical of 6 equals 6, confirming that 6 factors as the product of its distinct primes 2 and 3. Number theorists applying arithmetic functions to square-free integers or Möbius inversion would reference this verification. The proof is a direct native decision that evaluates the radical definition at 6.
Claim. $rad(6) = 6$, where $rad(n)$ denotes the product of the distinct prime factors of $n$.
background
The radical function is defined as the product of distinct prime factors of a natural number n. This module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function to support Dirichlet inversion once interfaces stabilize. The upstream definition states that the radical of n is the product of its distinct prime factors.
proof idea
One-line term proof that applies native_decide to evaluate the radical definition directly at 6.
why it matters
This equality supplies a concrete base case for the radical function inside the arithmetic-functions layer. The layer underpins Möbius properties and square-free checks that feed number-theoretic tools used across the Recognition framework, including prime-factor handling in mass formulas and forcing-chain steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.