squarefree_fifteen
plain-language theorem explainer
The declaration asserts that the integer 15 is squarefree. Number theorists applying the Möbius function to arithmetic computations would cite this basic instance. The proof proceeds as a direct computational check via native decision procedure on the prime factorization.
Claim. $15$ is square-free, that 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 μ. Squarefreeness is the predicate that a positive integer has no squared prime factor in its factorization. This instance for 15 is stated independently of deeper Dirichlet inversion.
proof idea
The proof is a one-line term that invokes native_decide to evaluate the squarefree predicate on 15 by direct factorization check.
why it matters
The result supplies a concrete squarefree instance that supports Möbius function applications in the same module. It fills a basic arithmetic foothold without new hypotheses or connection to the forcing chain T0-T8. No downstream theorems are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.