squarefree_thirtyfive
plain-language theorem explainer
The theorem establishes that 35 factors as 5 times 7 with no repeated prime powers. Number theorists applying Möbius inversion or checking arithmetic function values at small composites would reference this instance. The proof is a one-line native_decide tactic that evaluates the squarefreeness predicate by direct computation.
Claim. The integer 35 is square-free, i.e., its prime factorization $35 = 5^1 7^1$ contains no prime raised to an exponent greater than one.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function μ (denoted ArithmeticFunction.moebius). Squarefreeness is the predicate that an integer n is not divisible by p² for any prime p; this is equivalent to μ(n) ≠ 0. The file imports Basic and Squarefree modules to support such concrete checks before layering Dirichlet inversion.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the Squarefree predicate on 35.
why it matters
This supplies a concrete base case inside the arithmetic-functions section that feeds Möbius-related lemmas such as mobius_ne_zero_iff_squarefree. It fills a small but necessary instance in the NumberTheory.Primes hierarchy without invoking the Recognition Science forcing chain or constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.