E1_zero
plain-language theorem explainer
The genus-one Weierstrass factor satisfies E₁(0) = 1 by direct substitution. Analysts constructing Hadamard products for order-one entire functions invoke this identity when initializing products at the origin or verifying normalization. The proof is a one-line simplification that unfolds the explicit definition.
Claim. For the genus-one Weierstrass factor $E_1(z) := (1 - z) e^z$ with $z$ complex, the identity $E_1(0) = 1$ holds.
background
Module NumberTheory.HadamardGenusOne supplies the analytic substrate for the genus-one Hadamard factorization of entire functions of order at most one. Mathlib does not package the full theorem, so the module proves the unconditional properties of the elementary factor $E_1(z) = (1 - z) e^z$: norm bounds, summability of corrections $E_1(z_n) - 1$ from summability of $|z_n|^2$, and multipliability of partial products. The local setting is therefore the preparatory estimates needed before the three open questions listed in the module documentation can be addressed.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of E1.
why it matters
This identity normalizes the partial products that appear in the Hadamard construction for the completed Riemann zeta function. It supports the summability and multipliability results that follow in the same module and fills the most elementary slot among the analytic prerequisites. The module documentation explicitly flags the three remaining open pieces: XiOrderBound, XiZeroSummability, and XiHadamardIdentification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.