dirichletOne_ne_one
plain-language theorem explainer
The Dirichlet unit function ε vanishes at every natural number n different from one. Number theorists working with Dirichlet series or Möbius inversion cite this identity as the base case for convolution calculations. The proof reduces immediately to the definition via a single simplification step.
Claim. Let $ε$ denote the Dirichlet unit function on the natural numbers. For every natural number $n ≠ 1$, one has $ε(n) = 0$.
background
The module supplies lightweight wrappers around Mathlib arithmetic functions, beginning with the Möbius function μ. The local setting prepares basic interfaces for Dirichlet algebra and inversion once the definitions stabilize. Upstream results supply structures for ledger factorization and spectral emergence that embed these number-theoretic primitives inside the Recognition framework.
proof idea
The proof is a one-line wrapper that applies simp to the definition of dirichletOne together with the hypothesis n ≠ 1.
why it matters
This result records the vanishing property of the Dirichlet unit function ε, a prerequisite for arithmetic identities in the primes module. It supports later Möbius and prime-factorization steps that feed into the forcing chain. The declaration has no downstream uses recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.