dirichletOne_def
plain-language theorem explainer
The declaration establishes that the Dirichlet unit function equals the constant arithmetic function 1. Number theorists applying arithmetic functions to Dirichlet convolution identities would cite this to simplify unit-element reductions. The proof is a direct reflexivity step that matches the abbreviation definition without additional lemmas.
Claim. The Dirichlet unit function satisfies $ε = 1$, where $1$ denotes the multiplicative identity in the ring of arithmetic functions.
background
This module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ and the Dirichlet unit. The Dirichlet unit ε (also written δ_1) is the identity element for Dirichlet convolution: it takes the value 1 at n=1 and 0 at all other positive integers. The abbreviation dirichletOne wraps this unit directly as the constant 1 in the ArithmeticFunction ℤ type.
proof idea
The proof is a term-mode reflexivity step. It applies rfl directly to the defining abbreviation dirichletOne := 1, confirming the equality by definition.
why it matters
This result supplies the identity element required for the Dirichlet ring structure in the arithmetic-functions interface. It supports later Möbius inversion steps referenced in the module documentation, though no downstream uses are recorded yet. The equality closes the basic definitional layer before deeper algebra is layered on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.