ThmDex – An index of mathematical definitions, results, and conjectures.
 ▼ Set of symbols ▼ Alphabet ▼ Deduction system ▼ Theory ▼ Zermelo-Fraenkel set theory ▼ Set ▼ Binary cartesian set product ▼ Binary relation ▼ Map ▼ Operation ▼ N-operation ▼ Binary operation ▼ Enclosed binary operation ▼ Groupoid ▼ Semigroup ▼ Monoid ▼ Multiplicative monoid of integers ▼ Multiplicative monoid of natural numbers
Definition D6
Natural number factorial function

Let $\mathbb{N}$ be the D225: Set of natural numbers.
The natural number factorial function is the D4949: Natural number function $$\mathbb{N} \to \mathbb{N}, \quad N \mapsto \begin{cases} \prod_{n = 1}^N n, \quad & N > 0 \\ 1, \quad & N = 0 \end{cases}$$

Let $\mathbb{N}$ be the D225: Set of natural numbers.
The natural number factorial function is the D4949: Natural number function $$\mathbb{N} \to \mathbb{N}, \quad N \mapsto I_{N > 0} \left( \prod_{n = 1}^N n \right) + I_{N = 0}$$
Children
 ▶ Basic natural number factorial ▶ Factorial sequence
Results
 ▶ R4898 ▶ R4899 ▶ Natural number factorial is an even number for numbers 2 or greater ▶ Trivial factorial upper bound ▶ Weak Stirling formula