arithId_isMultiplicative
plain-language theorem explainer
The identity arithmetic function id(n) = n is multiplicative. Number theorists working with Dirichlet convolution or inversion formulas cite this as a standard base case. The proof is a one-line term reduction that unfolds the definition and matches Mathlib's built-in multiplicativity result for the identity.
Claim. Let $id : ℕ → ℕ$ be the function given by $id(n) = n$. Then $id$ is multiplicative: $id(mn) = id(m) ⋅ id(n)$ whenever $m, n$ are coprime natural numbers.
background
Arithmetic functions are maps from natural numbers to numbers that support Dirichlet convolution. The module supplies lightweight wrappers around Mathlib's arithmetic function library, beginning with the Möbius function μ. The identity arithmetic function is defined by id(n) = n. This result confirms its multiplicativity, relying on that definition together with the standard notion of multiplicative functions. The module context prepares for deeper Dirichlet algebra and inversion once basic interfaces stabilize.
proof idea
The proof is a term-mode reduction: it simplifies using the definition of the identity arithmetic function and then directly invokes Mathlib's theorem that the identity arithmetic function is multiplicative.
why it matters
This establishes the multiplicativity of the identity arithmetic function as a foundational property in the arithmetic functions module. It supports later constructions such as the Möbius function and prime counting. In the Recognition Science framework it supplies a basic number-theoretic tool, though no immediate downstream theorems depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.