Euler's sine product

Remarks

The convergence follows from $\sum_n \abs{z}^2 / n^2 < \infty$. Both sides are entire functions with simple zeros exactly at the integers. By the Weierstrass factorization theorem, their quotient is $e^{g(z)}$ for an entire function $g$. One shows that $g$ is constant, for example by comparing logarithmic derivatives with the partial fraction expansion $\pi \cot(\pi z) = \frac{1}{z} + \sum_{n \ge 1} \frac{2z}{z^2 - n^2}$; the limit at $z = 0$ then gives $e^{g} = 1$. Comparing the coefficients of $z^3$ on both sides gives $\sum_{n \ge 1} 1/n^2 = \pi^2/6$, the Basel problem. At $z = 1/2$ it gives the Wallis product $\frac{2}{\pi} = \prod_{n \ge 1} \left(1 - \frac{1}{4n^2}\right)$. In Mathlib it is Complex.tendsto_euler_sin_prod.

Going deeper

For a student

The formula is the standard example of a Weierstrass product. Here no exponential correction factors are needed, because the factors $1 - z/n$ and $1 + z/n$ are paired. Taking the logarithmic derivative gives the partial fraction expansion of $\pi\cot(\pi z)$. Combined with the product for $1/\Gamma$, it yields the reflection formula for the gamma function.