dirichletOne_one
plain-language theorem explainer
The Dirichlet unit function ε satisfies ε(1) = 1 by direct evaluation from its definition. Number theorists working with Dirichlet convolution cite this as the base case for the multiplicative identity in the arithmetic functions ring. The proof is a one-line simplification that unfolds the definition of dirichletOne.
Claim. Let ε denote the Dirichlet unit function. Then ε(1) = 1.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, starting with the Möbius function μ and the Dirichlet unit ε. Local setting is the ring of arithmetic functions under Dirichlet convolution, where ε serves as the multiplicative identity. Upstream, dirichletOne is the abbrev wrapping ε = δ_1, the function that equals 1 at argument 1.
proof idea
The proof is a one-line wrapper that applies simp on the definition of dirichletOne.
why it matters
This closes the base case for the Dirichlet unit inside the arithmetic functions module. It supports later Dirichlet inversion and convolution work in the NumberTheory layer of Recognition Science. No downstream uses are recorded yet, leaving the unit property available for extension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.