radical_twohundredten
plain-language theorem explainer
The equality rad(210) = 210 holds because 210 factors as the product of four distinct primes. Number theorists checking square-freeness via arithmetic functions would cite this explicit instance. The proof is a one-line native_decide evaluation of the radical definition.
Claim. $rad(210) = 210$, where $rad(n)$ is the product of the distinct prime factors of $n$.
background
The radical function is defined as the product of the distinct prime factors of its argument. This module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function and keeping statements minimal until Dirichlet inversion layers stabilize. The upstream radical definition states that rad(n) equals the product over the prime factors of n.
proof idea
The proof is a one-line term that invokes native_decide to evaluate the equality by direct computation of the prime factorization of 210.
why it matters
This theorem supplies a concrete square-free check inside the arithmetic functions layer of the primes module. It supports the Recognition Science number-theory scaffolding that feeds Möbius-based inversion steps. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.