Fungrim entry: def588

Symbol: Binomial —

{n \choose k}

— Binomial coefficient

Domain	Codomain
$n \in \mathbb{Z}_{\ge 0} \,\mathbin{\operatorname{and}}\, k \in \mathbb{Z}_{\ge 0}$	${n \choose k} \in \mathbb{Z}_{\ge 0}$
$n \in \mathbb{C} \,\mathbin{\operatorname{and}}\, k \in \mathbb{Z}_{\ge 0}$	${n \choose k} \in \mathbb{C}$

Table data:

\left(P, Q\right)

such that

\left(P\right) \implies \left(Q\right)

Definitions:

Fungrim symbol	Notation	Short description
`Binomial`	${n \choose k}$	Binomial coefficient
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("def588"),
    SymbolDefinition(Binomial, Binomial(n, k), "Binomial coefficient"),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(And(Element(n, ZZGreaterEqual(0)), Element(k, ZZGreaterEqual(0))), Element(Binomial(n, k), ZZGreaterEqual(0))), Tuple(And(Element(n, CC), Element(k, ZZGreaterEqual(0))), Element(Binomial(n, k), CC)))))

Topics using this entry

Factorials and binomial coefficients