squarefree_six
plain-language theorem explainer
The theorem asserts that the integer 6 has no squared prime factors. Number theorists applying Möbius inversion to small composites would cite this fact when checking the support of arithmetic functions. The proof is a one-line native decision procedure that computes the predicate directly from the definition.
Claim. The positive integer 6 is square-free, meaning it is not divisible by $p^2$ for any prime $p$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Square-freeness is the predicate that an integer has no repeated prime factors, a prerequisite for μ(n) ≠ 0. The local setting keeps statements minimal before layering Dirichlet algebra or inversion formulas.
proof idea
The proof is a one-line wrapper that applies native_decide to the predicate Squarefree 6.
why it matters
This supplies a basic arithmetic fact inside the Möbius footholds layer. It supports later inversion steps in the Recognition framework's number-theoretic components, though it carries no direct link to forcing chains or constants. No parent theorems or open questions are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.