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
Natural number factorial function
Formulation 0
Let $\mathbb{N}$ be the D225: Set of natural numbers.
The natural number factorial function is the D4949: Natural number function \begin{equation} \mathbb{N} \to \mathbb{N}, \quad N \mapsto \begin{cases} \prod_{n = 1}^N n, \quad & N > 0 \\ 1, \quad & N = 0 \end{cases} \end{equation}
Formulation 1
Let $\mathbb{N}$ be the D225: Set of natural numbers.
The natural number factorial function is the D4949: Natural number function \begin{equation} \mathbb{N} \to \mathbb{N}, \quad N \mapsto I_{N > 0} \left( \prod_{n = 1}^N n \right) + I_{N = 0} \end{equation}
Child definitions
» D2166: Basic natural number factorial
» D4689: Factorial sequence
Results
» R2589: Trivial factorial upper bound
» R2588: Weak Stirling formula
» R3: Stirling formula
» R4898:
» R4899:
» R5115: Natural number factorial is an even number for numbers 2 or greater