hadamardE1
plain-language theorem explainer
The definition supplies the genus-one elementary Hadamard factor E₁(z) = (1 - z) exp(z) for complex z. Analysts constructing Hadamard products for entire functions of order one, such as the completed Riemann zeta function, would reference this when building finite approximations over zeros. It is introduced as a direct algebraic expression without additional lemmas.
Claim. The genus-one elementary factor is defined by $E_1(z) := (1 - z) e^z$ for $z$ complex.
background
The HadamardFactorization module supplies the interface for a Hadamard product representation of the completed zeta function. Mathlib already provides the completed zeta function, its differentiability, and functional equation, but lacks the product form. This module defines the primary genus-one factor and partial products to enable later explicit-formula work.
proof idea
The definition is given directly by the algebraic expression (1 - z) * exp(z), matching the standard form of the genus-one Hadamard elementary factor.
why it matters
This definition serves as the atomic building block for the finite genus-one products over zeros, as used in hadamardPartialProduct and verified at zero in hadamardE1_zero. It fills the product interface required to identify the limit with completedRiemannZeta₀ in the RH closure plan.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.