squarefree_ten
plain-language theorem explainer
Ten is squarefree, with prime factorization containing no repeated factors. Number theorists building Möbius-based inversion in the Recognition Science arithmetic functions module would cite this instance when evaluating small integers. The proof executes as a direct computational check via the native decision tactic.
Claim. The positive integer 10 is square-free, i.e., not divisible by $p^2$ for any prime $p$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. Squarefreeness is the predicate that determines when μ(n) is nonzero, as seen in sibling definitions such as mobius_ne_zero_iff_squarefree. The local theoretical setting is the preparation of basic Dirichlet algebra interfaces for later inversion formulas.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the decidable proposition Squarefree 10 by direct factorization.
why it matters
This supplies a concrete base case for the squarefree predicate used to define the Möbius function in the arithmetic functions module. It supports the number-theoretic scaffolding required for Recognition Science constructions, though no downstream uses are recorded yet. It aligns with the basic arithmetic tools needed before applying the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.