mobius_def
plain-language theorem explainer
Equating the local Möbius wrapper to Mathlib's standard definition allows seamless use of classical arithmetic results inside the Recognition framework. Number theorists working on prime factorization and squarefree detection would cite this equivalence for compatibility with Möbius inversion. The proof reduces to a direct reflexivity step once the abbreviation is introduced.
Claim. Let $mu$ denote the Möbius function as an arithmetic function from natural numbers to integers. Then $mu$ coincides exactly with the standard Möbius arithmetic function defined in the library.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function $mu$ viewed as a map from natural numbers to integers. The upstream abbreviation declares mobius to be precisely ArithmeticFunction.moebius, establishing the interface before deeper Dirichlet algebra or inversion formulas are added. The local theoretical setting keeps statements minimal until the basic interfaces stabilize.
proof idea
The proof is a one-line wrapper that applies reflexivity to equate the local abbreviation with the Mathlib definition.
why it matters
This declaration supplies the foundational equivalence for the Möbius function in the NumberTheory.Primes.ArithmeticFunctions module. It supports later results on squarefree numbers and prime properties while aligning with the framework's reuse of standard arithmetic tools. No downstream uses are recorded yet, but the equivalence closes the interface to Mathlib for any future inversion steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.