dirichletOne
plain-language theorem explainer
The Dirichlet unit function is introduced as the arithmetic function that equals 1 at argument 1 and 0 elsewhere. Number theorists working with Dirichlet convolution and Möbius inversion would cite this wrapper. It is realized as a one-line abbreviation that directly assigns the unit element from the arithmetic function library.
Claim. Let $ε$ be the arithmetic function on positive integers with $ε(1)=1$ and $ε(n)=0$ for all $n≠1$.
background
This module supplies lightweight wrappers around Mathlib's arithmetic function library, starting with the Möbius function μ. The Dirichlet unit ε is the multiplicative identity under Dirichlet convolution, so that ε * f = f for any arithmetic function f. The module keeps statements lightweight to allow deeper Dirichlet algebra and inversion to be layered on once basic interfaces stabilize.
proof idea
The declaration is a one-line abbreviation that directly sets the Dirichlet unit to the unit element in the ArithmeticFunction type.
why it matters
This definition supports the basic properties ε(1)=1 and ε(n)=0 for n>1 that establish the identity element for Dirichlet convolution. It forms part of the arithmetic function toolkit that enables Möbius inversion steps in the Recognition Science framework. The module positions these wrappers as footholds for further Dirichlet algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.