Factorial

🅟 Mar 22, 2026

  🅤 Mar 22, 2026

DEF-FAC. Factorial.

The factorial of $n\in\N$, written $n!$, is defined recursively:

  1. \[0! = 1;\]
  2. \[n! = (n-1)!\cdot n\]

    for all $n\in\N^+$.

For $n\in\N^+$ we have

\[n! = \prod_{k=1}^n k.\]