Factorial
Definition
The factorial function \(! : \mathbb{N} \to \mathbb{Z}^{+}\) is a function defined for natural numbers recursively as:
\[ n! =
\begin{cases}
n \times (n - 1)! & n \neq 0 \\
1 & n = 0
\end{cases}\]
Hence, for example, \(5! = 5 \times 4 \times 3 \times 2 \times 1 \times 1 = 120\).