squarefree_twohundredten
plain-language theorem explainer
The theorem asserts that 210 is squarefree. Number theorists applying Möbius inversion or divisor sums in Recognition Science would cite this when handling the factorization 2×3×5×7. The proof reduces the claim to direct computational verification via native_decide.
Claim. The positive integer 210 is square-free.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. It keeps statements basic to allow later layering of Dirichlet algebra and inversion. The declaration appears under a section header on divisor counts for RS constants.
proof idea
The proof is a one-line term-mode wrapper that applies native_decide to evaluate the Squarefree predicate on 210.
why it matters
This supplies a concrete squarefree integer whose prime factors support divisor counts tied to RS constants. It fills a basic arithmetic foothold in the Möbius interface without downstream uses recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.