mobius_isMultiplicative
plain-language theorem explainer
The declaration establishes that the Möbius function satisfies the multiplicative property for arithmetic functions. Number theorists applying Dirichlet inversion or series expansions would cite this result. The proof is a one-line wrapper that unfolds the local abbreviation and invokes the corresponding Mathlib lemma.
Claim. The Möbius function $μ:ℕ→ℤ$ is multiplicative: $μ(mn)=μ(m)μ(n)$ whenever $m,n$ are coprime natural numbers.
background
The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ (implemented as ArithmeticFunction.moebius). The local definition mobius is an abbreviation for this standard function. The module keeps statements minimal so that deeper Dirichlet algebra and inversion formulas can be added once basic interfaces stabilize.
proof idea
The proof is a one-line wrapper. It simplifies using the definition of mobius, then applies the Mathlib lemma ArithmeticFunction.isMultiplicative_moebius directly.
why it matters
This theorem supplies the multiplicative property of the Möbius function as a basic foothold in the arithmetic functions module. It prepares the ground for Dirichlet inversion formulas that may connect to later developments in the Recognition Science framework, such as those involving complexity structures or spectral emergence. No immediate downstream uses are recorded, indicating it serves as foundational scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.