The Rogers–Ramanujan Identities

This entry formalises the Rogers--Ramanujan Identities: $$\begin{array}{rl}\sum _{k=-\mathrm{\infty }}^{\mathrm{\infty }}\frac{q^{k^2}}{\prod _{j=1}^k(1-q^j)}& ={(\prod _{n=0}^{\mathrm{\infty }}(1-q^{1+5n})(1-q^{4+5n}))}^{-1}\\ \sum _{k=-\mathrm{\infty }}^{\mathrm{\infty }}\frac{q^{k^2+k}}{\prod _{j=1}^k(1-q^j)}& ={(\prod _{n=0}^{\mathrm{\infty }}(1-q^{2+5n})(1-q^{3+5n}))}^{-1}\end{array}$$

The formalisation follows the elegant proof given in Andrews and Eriksson Integer Partitions, using the Jacobi triple product.