mobius_apply_of_squarefree
plain-language theorem explainer
The theorem asserts that the Möbius function μ(n) equals (-1) raised to the power of the total number of prime factors of n whenever n is squarefree. Number theorists applying Möbius inversion or Dirichlet series restricted to squarefree supports would cite this identity to simplify their sums. The proof is a one-line wrapper that unfolds the local mobius definition and invokes the corresponding Mathlib result.
Claim. If $n$ is squarefree then $μ(n) = (-1)^{Ω(n)}$, where $Ω(n)$ counts the prime factors of $n$ with multiplicity.
background
The module supplies lightweight wrappers around Mathlib's arithmetic functions, beginning with the Möbius function μ. A natural number n is squarefree precisely when no squared prime divides it, i.e., all exponents in its prime factorization are at most 1. The local mobius delegates directly to ArithmeticFunction.moebius.
proof idea
The proof is a one-line wrapper that applies simpa to unfold the local mobius definition and then invokes ArithmeticFunction.moebius_apply_of_squarefree on the Squarefree hypothesis.
why it matters
It is invoked by liouville_eq_mobius_of_squarefree to equate the Liouville and Möbius functions on squarefree arguments, and by mobius_sq_eq_one_iff_squarefree to characterize when μ(n)² equals 1. Within the Recognition Science framework the identity supplies a basic counting tool that can enter arguments over the phi-ladder or prime distributions, though no direct link to the T0-T8 forcing chain is stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.