squarefree_onehundredfive
plain-language theorem explainer
The declaration proves that 105 is squarefree by confirming its prime factorization consists of distinct primes. Number theorists applying the Möbius function to specific integers in arithmetic identities would reference this instance for verification in Dirichlet series or inversion. The proof is a one-line term that invokes native_decide to evaluate the squarefreeness predicate directly.
Claim. The positive integer $105$ is squarefree, meaning it is not divisible by $p^2$ for any prime $p$.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function. Squarefreeness determines where the Möbius function is nonzero, since it vanishes exactly on integers divisible by a square. The local setting keeps statements minimal to stabilize basic interfaces before layering Dirichlet algebra.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to compute the factorization of 105 and confirm all prime exponents equal one.
why it matters
This supplies a concrete verified instance inside the arithmetic functions module that supports Möbius footholds for later inversion work. It aligns with the NumberTheory domain by furnishing small facts needed for prime-related arithmetic. No downstream theorems cite it yet, leaving open whether it will feed explicit computations in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.