squarefree_seventy
plain-language theorem explainer
The theorem asserts that 70 factors as 2 times 5 times 7 with no repeated prime factors and is therefore squarefree. Number theorists applying the Möbius function to arithmetic inversion formulas would cite this concrete instance. The proof is a one-line term that delegates to native_decide for direct computational verification.
Claim. $70$ is square-free.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. Squarefree is the predicate asserting that an integer has no squared prime in its factorization, a prerequisite for many Möbius identities such as μ(n) ≠ 0 precisely when n is squarefree. The local setting is a collection of basic footholds for later Dirichlet algebra rather than a full development of inversion formulas.
proof idea
The proof is a term-mode one-liner that applies native_decide to evaluate the Squarefree predicate directly on the concrete integer 70.
why it matters
The result supplies a verified concrete squarefree integer inside the NumberTheory.Primes.ArithmeticFunctions module, supporting sibling statements about the Möbius function such as mobius_ne_zero_iff_squarefree. It fills a basic arithmetic fact in the lightweight interface described in the module doc-comment, with no downstream uses recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.