\begin{definition}[Definition:Factorial/Definition 1]
Let $n \in \Z_{\ge 0}$ be a positive integer.
The '''factorial of $n$''' is defined inductively as:
:$n! = \begin {cases}
1 & : n = 0 \\
n \paren {n - 1}! & : n > 0
\end {cases}$
\end{definition}