Reflection formula for the gamma function

Remarks

For $0 < \operatorname{Re} z < 1$, the product $\Gamma(z)\Gamma(1-z)$ equals the beta integral $\int_0^\infty \frac{t^{z-1}}{1+t}\,dt$. This integral is computed by the residue theorem, or for real $z$ by a substitution, and equals $\pi / \sin(\pi z)$. Both sides are meromorphic on $\C$, so the identity extends from the strip to all of $\C \setminus \Z$ by the identity theorem. Another proof multiplies the Weierstrass products of $1/\Gamma(z)$ and $1/\Gamma(1-z)$ and compares with Euler's sine product. At $z = 1/2$ the formula gives $\Gamma(1/2)^2 = \pi$, so $\Gamma(1/2) = \sqrt{\pi}$, because $\Gamma(1/2) > 0$. The integers are excluded: at each $n \in \Z$ one factor on the left has a pole and $\sin(\pi n) = 0$. In Mathlib it is Complex.Gamma_mul_Gamma_one_sub.

Going deeper

For a student

The right side $\pi/\sin(\pi z)$ is never $0$, so the formula shows that $\Gamma$ has no zeros off the integers. Since also $\Gamma(n) = (n-1)! \ne 0$ for $n \ge 1$, the function $1/\Gamma$ is entire with zeros exactly at $0, -1, -2, \ldots$. Together with the functional equation $\Gamma(z+1) = z\Gamma(z)$ and the duplication formula, it is one of the basic identities of the gamma function. It is used, for example, in the functional equation of the Riemann zeta function, where values of $\Gamma$ at $s/2$ and $(1-s)/2$ appear.