mobius_eq_zero_of_not_squarefree
If a natural number n is not squarefree then its Möbius function value vanishes. Number theorists applying Möbius inversion or Dirichlet convolution cite this property as a standard fact about the support of μ. The proof is a one-line wrapper that unfolds the local abbreviation for mobius and invokes the corresponding Mathlib result.
claimIf $n$ is not squarefree, then $μ(n)=0$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ defined as the abbreviation mobius := ArithmeticFunction.moebius. Squarefree n means n is not divisible by any square greater than 1. The local setting is a collection of small footholds for later Dirichlet algebra and inversion formulas.
proof idea
The proof is a one-line wrapper that applies ArithmeticFunction.moebius_eq_zero_of_not_squarefree after rewriting with the definition of mobius.
why it matters in Recognition Science
This theorem is invoked directly inside the proof of mobius_sq_eq_one_iff_squarefree, which states that μ(n)² = 1 if and only if n is squarefree. It supplies a basic arithmetic-function identity required for prime-counting arguments that appear in the Recognition Science number-theory layer.
scope and limits
- Does not compute explicit nonzero values of μ on squarefree inputs.
- Does not address the sign of μ when it is nonzero.
- Does not extend the statement to other arithmetic functions.
formal statement (Lean)
42theorem mobius_eq_zero_of_not_squarefree {n : ℕ} (h : ¬Squarefree n) : mobius n = 0 := by
proof body
Term-mode proof.
43 simpa [mobius] using (ArithmeticFunction.moebius_eq_zero_of_not_squarefree (n := n) h)
44
45/-- `μ n ≠ 0` iff `n` is squarefree. -/