Definition 1.8.1.49.  Let n, k ∈ . We define
(nk)
by:
(n0) := 1(0x + 1) := 0  (x ∈ )(m + 1x + 1) := (mx) + (mx + 1)  (m ∈ , x ∈ )
Remarks.

We use this definition of the binomial coefficient because it does not need any well-definedness proof. It can then easily be proved to be equal to the standard definition (see $"Binomial coefficient equality").

References.