not_squarefree_eighteen
plain-language theorem explainer
Eighteen fails to be squarefree because nine divides it. Number theorists working with the Möbius function would cite this instance when verifying where the function vanishes. The proof is a one-line native decision procedure that checks the square-divisor condition by direct computation.
Claim. The positive integer $18$ is not square-free.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function. Squarefreeness is the property that no square greater than one divides the integer; it controls the support of the Möbius function. This theorem records the concrete case n=18 where the property fails.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to reduce the statement to a decidable predicate and confirm it by computation.
why it matters
This supplies a basic fact for the arithmetic functions module and supports Möbius properties such as vanishing on non-squarefree arguments. It aligns with the lightweight interfaces needed before layering Dirichlet inversion. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.