squarefree_twentyone
plain-language theorem explainer
The declaration asserts that the integer 21 is squarefree. Number theorists using Möbius inversion over small integers would cite this fact when checking base cases in arithmetic functions. The proof is a one-line native decision procedure that evaluates the property directly.
Claim. The positive integer $21$ is square-free.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Squarefreeness serves as the condition under which the Möbius function is nonzero at an integer. The local setting keeps such statements minimal until deeper Dirichlet inversion is added.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the decidable proposition Squarefree 21.
why it matters
This fact populates the arithmetic-functions layer that supports Möbius footholds in the Recognition Science number-theory scaffolding. It supplies a concrete base case for later prime-related calculations but currently has no downstream citations. The module doc positions such results as preparatory for Dirichlet algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.