not_squarefree_twenty
plain-language theorem explainer
The number 20 fails to be squarefree because the square 4 divides it. Number theorists applying the Möbius function to arithmetic progressions would cite this instance to fix μ(20) at zero. The proof is a one-line native_decide tactic that evaluates the squarefree predicate by direct computation.
Claim. $20$ is not squarefree, since $4$ divides $20$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Squarefree is the predicate that a positive integer is not divisible by any square greater than 1. The local setting keeps statements minimal so that Dirichlet inversion and related algebra can be added once the basic interfaces are stable.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the decidable predicate Squarefree 20.
why it matters
This supplies a concrete base case for the Möbius function properties in the arithmetic-functions module, ensuring μ(20) evaluates to zero when a square divides the argument. It supports the Recognition Science number-theory layer that feeds into prime-related calculations, though no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.