mobius
plain-language theorem explainer
The Möbius function is introduced as a direct alias to Mathlib's standard arithmetic function, mapping natural numbers to integers. Number theorists building results on squarefree integers or Liouville-Möbius relations would cite this wrapper. The definition is a one-line abbreviation that reexports the library implementation without modification.
Claim. Let $μ : ℕ → ℤ$ denote the Möbius arithmetic function, obtained by reexporting the standard library definition.
background
Arithmetic functions are maps ℕ → R for a ring R; here the codomain is ℤ. The Möbius function μ(n) vanishes on non-squarefree arguments and equals (-1)^k on squarefree n with k distinct prime factors. The module supplies lightweight wrappers around Mathlib's library, beginning with this Möbius alias, to stabilize basic interfaces before adding Dirichlet inversion.
proof idea
One-line abbreviation that directly assigns ArithmeticFunction.moebius to the local identifier mobius.
why it matters
This alias anchors the arithmetic-functions section and is invoked by 28 downstream declarations, including liouville_eq_mobius_of_squarefree (which equates λ(n) = μ(n) for squarefree n) and the characterizations mobius_eq_zero_iff_not_squarefree together with mobius_apply_of_squarefree. It supplies the number-theoretic foothold needed for prime-related scaffolding in the Recognition framework, though it carries no direct link to the T0-T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.