Factorials and binomial coefficients

Symbol: Factorial —

n !

— Factorial

Domain	Codomain
$n \in \mathbb{Z}_{\ge 0}$	$n ! \in \mathbb{Z}_{\ge 1}$

Table data:

\left(P, Q\right)

such that

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

Definitions:

Fungrim symbol	Notation	Short description
`Factorial`	$n !$	Factorial
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("81aeba"),
    SymbolDefinition(Factorial, Factorial(n), "Factorial"),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(Element(n, ZZGreaterEqual(0)), Element(Factorial(n), ZZGreaterEqual(1))))))

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)))))

579595

Symbol: RisingFactorial —

\left(z\right)_{k}

— Rising factorial

Domain	Codomain
$z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}$	$\left(z\right)_{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
`RisingFactorial`	$\left(z\right)_{k}$	Rising factorial
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("579595"),
    SymbolDefinition(RisingFactorial, RisingFactorial(z, k), "Rising factorial"),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(And(Element(z, CC), Element(k, ZZGreaterEqual(0))), Element(RisingFactorial(z, k), CC)))))

3c2469

Symbol: FallingFactorial —

\left(z\right)^{\underline{k}}

— Falling factorial

Domain	Codomain
$z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}$	$\left(z\right)^{\underline{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
`FallingFactorial`	$\left(z\right)^{\underline{k}}$	Falling factorial
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("3c2469"),
    SymbolDefinition(FallingFactorial, FallingFactorial(z, k), "Falling factorial"),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(And(Element(z, CC), Element(k, ZZGreaterEqual(0))), Element(FallingFactorial(z, k), CC)))))

d12aa0

n ! = \text{A000142}\!\left(n\right)

Assumptions:

n \in \mathbb{Z}_{\ge 0}

References:

Sequence A000142 in Sloane's On-Line Encyclopedia of Integer Sequences (OEIS)

TeX:

n ! = \text{A000142}\!\left(n\right)

n \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Factorial`	$n !$	Factorial
`SloaneA`	$\text{A00000X}\!\left(n\right)$	Sequence X in Sloane's OEIS
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("d12aa0"),
    Formula(Equal(Factorial(n), SloaneA("A000142", n))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(0))))

3009a7

Table of

n !

for

0 \le n \le 30

$n$	$n !$
0	1
1	1
2	2
3	6
4	24
5	120
6	720
7	5040
8	40320
9	362880
10	3628800
11	39916800
12	479001600
13	6227020800
14	87178291200

$n$	$n !$
15	1307674368000
16	20922789888000
17	355687428096000
18	6402373705728000
19	121645100408832000
20	2432902008176640000
21	51090942171709440000
22	1124000727777607680000
23	25852016738884976640000
24	620448401733239439360000
25	15511210043330985984000000
26	403291461126605635584000000
27	10888869450418352160768000000
28	304888344611713860501504000000
29	8841761993739701954543616000000
30	265252859812191058636308480000000

Definitions:

Fungrim symbol	Notation	Short description
`Factorial`	$n !$	Factorial

Source code for this entry:

Entry(ID("3009a7"),
    Description("Table of", Factorial(n), "for", LessEqual(0, n, 30)),
    Table(Var(n), TableValueHeadings(n, Factorial(n)), TableSplit(2), List(Tuple(0, 1), Tuple(1, 1), Tuple(2, 2), Tuple(3, 6), Tuple(4, 24), Tuple(5, 120), Tuple(6, 720), Tuple(7, 5040), Tuple(8, 40320), Tuple(9, 362880), Tuple(10, 3628800), Tuple(11, 39916800), Tuple(12, 479001600), Tuple(13, 6227020800), Tuple(14, 87178291200), Tuple(15, 1307674368000), Tuple(16, 20922789888000), Tuple(17, 355687428096000), Tuple(18, 6402373705728000), Tuple(19, 121645100408832000), Tuple(20, 2432902008176640000), Tuple(21, 51090942171709440000), Tuple(22, 1124000727777607680000), Tuple(23, 25852016738884976640000), Tuple(24, 620448401733239439360000), Tuple(25, 15511210043330985984000000), Tuple(26, 403291461126605635584000000), Tuple(27, 10888869450418352160768000000), Tuple(28, 304888344611713860501504000000), Tuple(29, 8841761993739701954543616000000), Tuple(30, 265252859812191058636308480000000))))

fb5d88

Table of

{n \choose k}

for

0 \le n \le 15

and

0 \le k \le 15

$n$ \ $k$	0	1	2	3	4	5	6	7	8	9	10	11	12	13	14	15
0	1	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
1	1	1	0	0	0	0	0	0	0	0	0	0	0	0	0	0
2	1	2	1	0	0	0	0	0	0	0	0	0	0	0	0	0
3	1	3	3	1	0	0	0	0	0	0	0	0	0	0	0	0
4	1	4	6	4	1	0	0	0	0	0	0	0	0	0	0	0
5	1	5	10	10	5	1	0	0	0	0	0	0	0	0	0	0
6	1	6	15	20	15	6	1	0	0	0	0	0	0	0	0	0
7	1	7	21	35	35	21	7	1	0	0	0	0	0	0	0	0
8	1	8	28	56	70	56	28	8	1	0	0	0	0	0	0	0
9	1	9	36	84	126	126	84	36	9	1	0	0	0	0	0	0
10	1	10	45	120	210	252	210	120	45	10	1	0	0	0	0	0
11	1	11	55	165	330	462	462	330	165	55	11	1	0	0	0	0
12	1	12	66	220	495	792	924	792	495	220	66	12	1	0	0	0
13	1	13	78	286	715	1287	1716	1716	1287	715	286	78	13	1	0	0
14	1	14	91	364	1001	2002	3003	3432	3003	2002	1001	364	91	14	1	0
15	1	15	105	455	1365	3003	5005	6435	6435	5005	3003	1365	455	105	15	1

Table data:

\left(n, k, y\right)

such that

{n \choose k} = y

Definitions:

Fungrim symbol	Notation	Short description
`Binomial`	${n \choose k}$	Binomial coefficient

Source code for this entry:

Entry(ID("fb5d88"),
    Description("Table of", Binomial(n, k), "for", LessEqual(0, n, 15), "and", LessEqual(0, k, 15)),
    Table(TableRelation(Tuple(n, k, y), Equal(Binomial(n, k), y)), TableHeadings(Description(n, "\", k), 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15), TableColumnHeadings(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15), List(Tuple(1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0), Tuple(1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0), Tuple(1, 2, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0), Tuple(1, 3, 3, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0), Tuple(1, 4, 6, 4, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0), Tuple(1, 5, 10, 10, 5, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0), Tuple(1, 6, 15, 20, 15, 6, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0), Tuple(1, 7, 21, 35, 35, 21, 7, 1, 0, 0, 0, 0, 0, 0, 0, 0), Tuple(1, 8, 28, 56, 70, 56, 28, 8, 1, 0, 0, 0, 0, 0, 0, 0), Tuple(1, 9, 36, 84, 126, 126, 84, 36, 9, 1, 0, 0, 0, 0, 0, 0), Tuple(1, 10, 45, 120, 210, 252, 210, 120, 45, 10, 1, 0, 0, 0, 0, 0), Tuple(1, 11, 55, 165, 330, 462, 462, 330, 165, 55, 11, 1, 0, 0, 0, 0), Tuple(1, 12, 66, 220, 495, 792, 924, 792, 495, 220, 66, 12, 1, 0, 0, 0), Tuple(1, 13, 78, 286, 715, 1287, 1716, 1716, 1287, 715, 286, 78, 13, 1, 0, 0), Tuple(1, 14, 91, 364, 1001, 2002, 3003, 3432, 3003, 2002, 1001, 364, 91, 14, 1, 0), Tuple(1, 15, 105, 455, 1365, 3003, 5005, 6435, 6435, 5005, 3003, 1365, 455, 105, 15, 1))))

29741c

Table of

\left(n\right)_{k}

for

0 \le n \le 10

and

0 \le k \le 10

$n$ \ $k$	0	1	2	3	4	5	6	7	8	9	10
0	1	0	0	0	0	0	0	0	0	0	0
1	1	1	2	6	24	120	720	5040	40320	362880	3628800
2	1	2	6	24	120	720	5040	40320	362880	3628800	39916800
3	1	3	12	60	360	2520	20160	181440	1814400	19958400	239500800
4	1	4	20	120	840	6720	60480	604800	6652800	79833600	1037836800
5	1	5	30	210	1680	15120	151200	1663200	19958400	259459200	3632428800
6	1	6	42	336	3024	30240	332640	3991680	51891840	726485760	10897286400
7	1	7	56	504	5040	55440	665280	8648640	121080960	1816214400	29059430400
8	1	8	72	720	7920	95040	1235520	17297280	259459200	4151347200	70572902400
9	1	9	90	990	11880	154440	2162160	32432400	518918400	8821612800	158789030400
10	1	10	110	1320	17160	240240	3603600	57657600	980179200	17643225600	335221286400

Table data:

\left(n, k, y\right)

such that

\left(n\right)_{k} = y

Definitions:

Fungrim symbol	Notation	Short description
`RisingFactorial`	$\left(z\right)_{k}$	Rising factorial

Source code for this entry:

Entry(ID("29741c"),
    Description("Table of", RisingFactorial(n, k), "for", LessEqual(0, n, 10), "and", LessEqual(0, k, 10)),
    Table(TableRelation(Tuple(n, k, y), Equal(RisingFactorial(n, k), y)), TableHeadings(Description(n, "\", k), 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10), TableColumnHeadings(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10), List(Tuple(1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0), Tuple(1, 1, 2, 6, 24, 120, 720, 5040, 40320, 362880, 3628800), Tuple(1, 2, 6, 24, 120, 720, 5040, 40320, 362880, 3628800, 39916800), Tuple(1, 3, 12, 60, 360, 2520, 20160, 181440, 1814400, 19958400, 239500800), Tuple(1, 4, 20, 120, 840, 6720, 60480, 604800, 6652800, 79833600, 1037836800), Tuple(1, 5, 30, 210, 1680, 15120, 151200, 1663200, 19958400, 259459200, 3632428800), Tuple(1, 6, 42, 336, 3024, 30240, 332640, 3991680, 51891840, 726485760, 10897286400), Tuple(1, 7, 56, 504, 5040, 55440, 665280, 8648640, 121080960, 1816214400, 29059430400), Tuple(1, 8, 72, 720, 7920, 95040, 1235520, 17297280, 259459200, 4151347200, 70572902400), Tuple(1, 9, 90, 990, 11880, 154440, 2162160, 32432400, 518918400, 8821612800, 158789030400), Tuple(1, 10, 110, 1320, 17160, 240240, 3603600, 57657600, 980179200, 17643225600, 335221286400))))

63f368

Table of

\left(n\right)^{\underline{k}}

for

0 \le n \le 10

and

0 \le k \le 10

$n$ \ $k$	0	1	2	3	4	5	6	7	8	9	10
0	1	0	0	0	0	0	0	0	0	0	0
1	1	1	0	0	0	0	0	0	0	0	0
2	1	2	2	0	0	0	0	0	0	0	0
3	1	3	6	6	0	0	0	0	0	0	0
4	1	4	12	24	24	0	0	0	0	0	0
5	1	5	20	60	120	120	0	0	0	0	0
6	1	6	30	120	360	720	720	0	0	0	0
7	1	7	42	210	840	2520	5040	5040	0	0	0
8	1	8	56	336	1680	6720	20160	40320	40320	0	0
9	1	9	72	504	3024	15120	60480	181440	362880	362880	0
10	1	10	90	720	5040	30240	151200	604800	1814400	3628800	3628800

Table data:

\left(n, k, y\right)

such that

\left(n\right)^{\underline{k}} = y

Definitions:

Fungrim symbol	Notation	Short description
`FallingFactorial`	$\left(z\right)^{\underline{k}}$	Falling factorial

Source code for this entry:

Entry(ID("63f368"),
    Description("Table of", FallingFactorial(n, k), "for", LessEqual(0, n, 10), "and", LessEqual(0, k, 10)),
    Table(TableRelation(Tuple(n, k, y), Equal(FallingFactorial(n, k), y)), TableHeadings(Description(n, "\", k), 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10), TableColumnHeadings(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10), List(Tuple(1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0), Tuple(1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0), Tuple(1, 2, 2, 0, 0, 0, 0, 0, 0, 0, 0), Tuple(1, 3, 6, 6, 0, 0, 0, 0, 0, 0, 0), Tuple(1, 4, 12, 24, 24, 0, 0, 0, 0, 0, 0), Tuple(1, 5, 20, 60, 120, 120, 0, 0, 0, 0, 0), Tuple(1, 6, 30, 120, 360, 720, 720, 0, 0, 0, 0), Tuple(1, 7, 42, 210, 840, 2520, 5040, 5040, 0, 0, 0), Tuple(1, 8, 56, 336, 1680, 6720, 20160, 40320, 40320, 0, 0), Tuple(1, 9, 72, 504, 3024, 15120, 60480, 181440, 362880, 362880, 0), Tuple(1, 10, 90, 720, 5040, 30240, 151200, 604800, 1814400, 3628800, 3628800))))

55bf43

n ! = \prod_{k=1}^{n} k

Assumptions:

n \in \mathbb{Z}_{\ge 0}

TeX:

n \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Factorial`	$n !$	Factorial
`Product`	$\prod_{n} f(n)$	Product
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("55bf43"),
    Equal(Factorial(n), Product(k, For(k, 1, n))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(0))))

788fa4

{z \choose k} = \prod_{i=1}^{k} \frac{z + 1 - i}{i} = \prod_{i=0}^{k - 1} \frac{z - i}{i + 1}

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

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

Source code for this entry:

Entry(ID("788fa4"),
    Equal(Binomial(z, k), Product(Div(Sub(Add(z, 1), i), i), For(i, 1, k)), Product(Div(Sub(z, i), Add(i, 1)), For(i, 0, Sub(k, 1)))),
    Variables(z, k),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)))))

19f13b

\left(z\right)_{k} = \prod_{i=1}^{k} \left(z + i - 1\right) = \prod_{i=0}^{k - 1} \left(z + i\right)

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`RisingFactorial`	$\left(z\right)_{k}$	Rising factorial
`Product`	$\prod_{n} f(n)$	Product
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("19f13b"),
    Equal(RisingFactorial(z, k), Product(Parentheses(Sub(Add(z, i), 1)), For(i, 1, k)), Product(Parentheses(Add(z, i)), For(i, 0, Sub(k, 1)))),
    Variables(z, k),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)))))

a5852d

\left(z\right)^{\underline{k}} = \prod_{i=1}^{k} \left(z - i + 1\right) = \prod_{i=0}^{k - 1} \left(z - i\right)

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`FallingFactorial`	$\left(z\right)^{\underline{k}}$	Falling factorial
`Product`	$\prod_{n} f(n)$	Product
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("a5852d"),
    Equal(FallingFactorial(z, k), Product(Parentheses(Add(Sub(z, i), 1)), For(i, 1, k)), Product(Parentheses(Sub(z, i)), For(i, 0, Sub(k, 1)))),
    Variables(z, k),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)))))

4f20ff

n ! = n \left(n - 1\right)!

Assumptions:

n \in \mathbb{Z}_{\ge 1}

TeX:

n ! = n \left(n - 1\right)!

n \in \mathbb{Z}_{\ge 1}

Definitions:

Fungrim symbol	Notation	Short description
`Factorial`	$n !$	Factorial
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("4f20ff"),
    Formula(Equal(Factorial(n), Mul(n, Factorial(Sub(n, 1))))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(1))))

2362af

{n \choose k} = {n \choose n - k}

Assumptions:

n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; k \in \{0, 1, \ldots, n\}

TeX:

{n \choose k} = {n \choose n - k}

n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; k \in \{0, 1, \ldots, n\}

Definitions:

Fungrim symbol	Notation	Short description
`Binomial`	${n \choose k}$	Binomial coefficient
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`Range`	$\{a, a + 1, \ldots, b\}$	Integers between given endpoints

Source code for this entry:

Entry(ID("2362af"),
    Formula(Equal(Binomial(n, k), Binomial(n, Sub(n, k)))),
    Variables(n, k),
    Assumptions(And(Element(n, ZZGreaterEqual(0)), Element(k, Range(0, n)))))

081188

{z + 1 \choose k + 1} = {z \choose k} + {z \choose k + 1}

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

{z + 1 \choose k + 1} = {z \choose k} + {z \choose k + 1}

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

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

Source code for this entry:

Entry(ID("081188"),
    Formula(Equal(Binomial(Add(z, 1), Add(k, 1)), Add(Binomial(z, k), Binomial(z, Add(k, 1))))),
    Variables(z, k),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)))))

209fc8

{z \choose k + 1} = \frac{z - k}{k + 1} {z \choose k}

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

{z \choose k + 1} = \frac{z - k}{k + 1} {z \choose k}

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

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

Source code for this entry:

Entry(ID("209fc8"),
    Formula(Equal(Binomial(z, Add(k, 1)), Mul(Div(Sub(z, k), Add(k, 1)), Binomial(z, k)))),
    Variables(z, k),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)))))

6e1f13

{z + 1 \choose k + 1} = \frac{z + 1}{k + 1} {z \choose k}

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

{z + 1 \choose k + 1} = \frac{z + 1}{k + 1} {z \choose k}

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

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

Source code for this entry:

Entry(ID("6e1f13"),
    Formula(Equal(Binomial(Add(z, 1), Add(k, 1)), Mul(Div(Add(z, 1), Add(k, 1)), Binomial(z, k)))),
    Variables(z, k),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)))))

56d4ff

{z \choose k} = {\left(-1\right)}^{k} {k - z - 1 \choose k}

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

{z \choose k} = {\left(-1\right)}^{k} {k - z - 1 \choose k}

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

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

Source code for this entry:

Entry(ID("56d4ff"),
    Formula(Equal(Binomial(z, k), Mul(Pow(-1, k), Binomial(Sub(Sub(k, z), 1), k)))),
    Variables(z, k),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)))))

02ee06

\left(z\right)_{k + m} = \left(z\right)_{k} \left(z + k\right)_{m}

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; m \in \mathbb{Z}_{\ge 0}

TeX:

\left(z\right)_{k + m} = \left(z\right)_{k} \left(z + k\right)_{m}

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; m \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`RisingFactorial`	$\left(z\right)_{k}$	Rising factorial
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("02ee06"),
    Formula(Equal(RisingFactorial(z, Add(k, m)), Mul(RisingFactorial(z, k), RisingFactorial(Add(z, k), m)))),
    Variables(z, k, m),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)), Element(m, ZZGreaterEqual(0)))))

d651d1

\left(z\right)_{2 k} = {4}^{k} \left(\frac{z}{2}\right)_{k} \left(\frac{z + 1}{2}\right)_{k}

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

\left(z\right)_{2 k} = {4}^{k} \left(\frac{z}{2}\right)_{k} \left(\frac{z + 1}{2}\right)_{k}

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`RisingFactorial`	$\left(z\right)_{k}$	Rising factorial
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("d651d1"),
    Formula(Equal(RisingFactorial(z, Mul(2, k)), Mul(Mul(Pow(4, k), RisingFactorial(Div(z, 2), k)), RisingFactorial(Div(Add(z, 1), 2), k)))),
    Variables(z, k),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)))))

c640bf

\left(-z\right)_{k} = {\left(-1\right)}^{k} \left(z - k + 1\right)_{k}

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

\left(-z\right)_{k} = {\left(-1\right)}^{k} \left(z - k + 1\right)_{k}

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`RisingFactorial`	$\left(z\right)_{k}$	Rising factorial
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("c640bf"),
    Formula(Equal(RisingFactorial(Neg(z), k), Mul(Pow(-1, k), RisingFactorial(Add(Sub(z, k), 1), k)))),
    Variables(z, k),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)))))

41f950

\left(z + 1\right)_{k} = \frac{z + k}{z} \left(z\right)_{k}

Assumptions:

z \in \mathbb{C} \setminus \left\{0\right\} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

\left(z + 1\right)_{k} = \frac{z + k}{z} \left(z\right)_{k}

z \in \mathbb{C} \setminus \left\{0\right\} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`RisingFactorial`	$\left(z\right)_{k}$	Rising factorial
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("41f950"),
    Formula(Equal(RisingFactorial(Add(z, 1), k), Mul(Div(Add(z, k), z), RisingFactorial(z, k)))),
    Variables(z, k),
    Assumptions(And(Element(z, SetMinus(CC, Set(0))), Element(k, ZZGreaterEqual(0)))))

fe9fb7

\left(z\right)_{k + 1} = \left(z + k\right) \left(z\right)_{k}

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

\left(z\right)_{k + 1} = \left(z + k\right) \left(z\right)_{k}

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`RisingFactorial`	$\left(z\right)_{k}$	Rising factorial
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("fe9fb7"),
    Formula(Equal(RisingFactorial(z, Add(k, 1)), Mul(Add(z, k), RisingFactorial(z, k)))),
    Variables(z, k),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)))))

62c6c9

n ! = \Gamma\!\left(n + 1\right)

Assumptions:

n \in \mathbb{Z}_{\ge 0}

TeX:

n ! = \Gamma\!\left(n + 1\right)

n \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Factorial`	$n !$	Factorial
`Gamma`	$\Gamma(z)$	Gamma function
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("62c6c9"),
    Formula(Equal(Factorial(n), Gamma(Add(n, 1)))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(0))))

e87c43

{z \choose k} = \frac{\Gamma\!\left(z + 1\right)}{\Gamma\!\left(k + 1\right) \Gamma\!\left(z - k + 1\right)}

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; z - k \notin \{-1, -2, \ldots\}

TeX:

{z \choose k} = \frac{\Gamma\!\left(z + 1\right)}{\Gamma\!\left(k + 1\right) \Gamma\!\left(z - k + 1\right)}

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; z - k \notin \{-1, -2, \ldots\}

Definitions:

Fungrim symbol	Notation	Short description
`Binomial`	${n \choose k}$	Binomial coefficient
`Gamma`	$\Gamma(z)$	Gamma function
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`ZZLessEqual`	$\mathbb{Z}_{\le n}$	Integers less than or equal to n

Source code for this entry:

Entry(ID("e87c43"),
    Formula(Equal(Binomial(z, k), Div(Gamma(Add(z, 1)), Mul(Gamma(Add(k, 1)), Gamma(Add(Sub(z, k), 1)))))),
    Variables(z, k),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)), NotElement(Sub(z, k), ZZLessEqual(-1)))))

332721

{n \choose k} = \frac{n !}{k ! \left(n - k\right)!}

Assumptions:

n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

{n \choose k} = \frac{n !}{k ! \left(n - k\right)!}

n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

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

Source code for this entry:

Entry(ID("332721"),
    Formula(Equal(Binomial(n, k), Div(Factorial(n), Mul(Factorial(k), Factorial(Sub(n, k)))))),
    Variables(n, k),
    Assumptions(And(Element(n, ZZGreaterEqual(0)), Element(k, ZZGreaterEqual(0)))))

1d5e92

{z \choose k} = \frac{\left(z\right)^{\underline{k}}}{k !}

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

{z \choose k} = \frac{\left(z\right)^{\underline{k}}}{k !}

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Binomial`	${n \choose k}$	Binomial coefficient
`FallingFactorial`	$\left(z\right)^{\underline{k}}$	Falling factorial
`Factorial`	$n !$	Factorial
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("1d5e92"),
    Formula(Equal(Binomial(z, k), Div(FallingFactorial(z, k), Factorial(k)))),
    Variables(z, k),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)))))

22ee07

{z \choose k} = \frac{\left(z - k + 1\right)_{k}}{k !}

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

{z \choose k} = \frac{\left(z - k + 1\right)_{k}}{k !}

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Binomial`	${n \choose k}$	Binomial coefficient
`RisingFactorial`	$\left(z\right)_{k}$	Rising factorial
`Factorial`	$n !$	Factorial
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("22ee07"),
    Formula(Equal(Binomial(z, k), Div(RisingFactorial(Add(Sub(z, k), 1), k), Factorial(k)))),
    Variables(z, k),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)))))

c733f7

\left(z\right)_{k} = \frac{\Gamma\!\left(z + k\right)}{\Gamma(z)}

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; z + k \notin \{0, -1, \ldots\}

TeX:

\left(z\right)_{k} = \frac{\Gamma\!\left(z + k\right)}{\Gamma(z)}

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; z + k \notin \{0, -1, \ldots\}

Definitions:

Fungrim symbol	Notation	Short description
`RisingFactorial`	$\left(z\right)_{k}$	Rising factorial
`Gamma`	$\Gamma(z)$	Gamma function
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`ZZLessEqual`	$\mathbb{Z}_{\le n}$	Integers less than or equal to n

Source code for this entry:

Entry(ID("c733f7"),
    Formula(Equal(RisingFactorial(z, k), Div(Gamma(Add(z, k)), Gamma(z)))),
    Variables(z, k),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)), NotElement(Add(z, k), ZZLessEqual(0)))))

e78989

\left(z\right)_{k} = \left(z + k - 1\right)^{\underline{k}}

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

\left(z\right)_{k} = \left(z + k - 1\right)^{\underline{k}}

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`RisingFactorial`	$\left(z\right)_{k}$	Rising factorial
`FallingFactorial`	$\left(z\right)^{\underline{k}}$	Falling factorial
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("e78989"),
    Formula(Equal(RisingFactorial(z, k), FallingFactorial(Sub(Add(z, k), 1), k))),
    Variables(z, k),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)))))

30652c

\left(n\right)_{k} = \frac{\left(n + k - 1\right)!}{\left(n - 1\right)!}

Assumptions:

n \in \mathbb{Z}_{\ge 1} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

\left(n\right)_{k} = \frac{\left(n + k - 1\right)!}{\left(n - 1\right)!}

n \in \mathbb{Z}_{\ge 1} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`RisingFactorial`	$\left(z\right)_{k}$	Rising factorial
`Factorial`	$n !$	Factorial
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("30652c"),
    Formula(Equal(RisingFactorial(n, k), Div(Factorial(Sub(Add(n, k), 1)), Factorial(Sub(n, 1))))),
    Variables(n, k),
    Assumptions(And(Element(n, ZZGreaterEqual(1)), Element(k, ZZGreaterEqual(0)))))

6f7746

\sum_{k=0}^{n} {n \choose k} {x}^{k} {y}^{n - k} = {\left(x + y\right)}^{n}

Assumptions:

x \in \mathbb{C} \;\mathbin{\operatorname{and}}\; y \in \mathbb{C} \;\mathbin{\operatorname{and}}\; n \in \mathbb{Z}_{\ge 0}

TeX:

\sum_{k=0}^{n} {n \choose k} {x}^{k} {y}^{n - k} = {\left(x + y\right)}^{n}

x \in \mathbb{C} \;\mathbin{\operatorname{and}}\; y \in \mathbb{C} \;\mathbin{\operatorname{and}}\; n \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Sum`	$\sum_{n} f(n)$	Sum
`Binomial`	${n \choose k}$	Binomial coefficient
`Pow`	${a}^{b}$	Power
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("6f7746"),
    Formula(Equal(Sum(Mul(Mul(Binomial(n, k), Pow(x, k)), Pow(y, Sub(n, k))), For(k, 0, n)), Pow(Add(x, y), n))),
    Variables(x, y, n),
    Assumptions(And(Element(x, CC), Element(y, CC), Element(n, ZZGreaterEqual(0)))))

7c014b

\sum_{k=0}^{\infty} {z \choose k} {x}^{k} = {\left(1 + x\right)}^{z}

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; x \in \mathbb{C} \;\mathbin{\operatorname{and}}\; \left|x\right| < 1

Alternative assumptions:

z \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; z \in \mathbb{C}

TeX:

\sum_{k=0}^{\infty} {z \choose k} {x}^{k} = {\left(1 + x\right)}^{z}

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; x \in \mathbb{C} \;\mathbin{\operatorname{and}}\; \left|x\right| < 1

z \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; z \in \mathbb{C}

Definitions:

Fungrim symbol	Notation	Short description
`Sum`	$\sum_{n} f(n)$	Sum
`Binomial`	${n \choose k}$	Binomial coefficient
`Pow`	${a}^{b}$	Power
`Infinity`	$\infty$	Positive infinity
`CC`	$\mathbb{C}$	Complex numbers
`Abs`	$\left\|z\right\|$	Absolute value
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("7c014b"),
    Formula(Equal(Sum(Mul(Binomial(z, k), Pow(x, k)), For(k, 0, Infinity)), Pow(Add(1, x), z))),
    Variables(z, x),
    Assumptions(And(Element(z, CC), Element(x, CC), Less(Abs(x), 1)), And(Element(z, ZZGreaterEqual(0)), Element(z, CC))))

858c8f

\sum_{k=0}^{n} {n \choose k} = {2}^{n}

Assumptions:

n \in \mathbb{Z}_{\ge 0}

TeX:

\sum_{k=0}^{n} {n \choose k} = {2}^{n}

n \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Sum`	$\sum_{n} f(n)$	Sum
`Binomial`	${n \choose k}$	Binomial coefficient
`Pow`	${a}^{b}$	Power
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("858c8f"),
    Formula(Equal(Sum(Binomial(n, k), For(k, 0, n)), Pow(2, n))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(0))))

4d1365

{z \choose k} = \sum_{i=0}^{k} s\!\left(k, i\right) \frac{{z}^{i}}{k !}

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

{z \choose k} = \sum_{i=0}^{k} s\!\left(k, i\right) \frac{{z}^{i}}{k !}

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Binomial`	${n \choose k}$	Binomial coefficient
`Sum`	$\sum_{n} f(n)$	Sum
`StirlingS1`	$s\!\left(n, k\right)$	Signed Stirling number of the first kind
`Pow`	${a}^{b}$	Power
`Factorial`	$n !$	Factorial
`CC`	$\mathbb{C}$	Complex numbers
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("4d1365"),
    Formula(Equal(Binomial(z, k), Sum(Mul(StirlingS1(k, i), Div(Pow(z, i), Factorial(k))), For(i, 0, k)))),
    Variables(z, k),
    Assumptions(And(Element(z, CC), Element(k, ZZGreaterEqual(0)))))

1635f5

{e}^{z} = \sum_{k=0}^{\infty} \frac{{z}^{k}}{k !}

Assumptions:

z \in \mathbb{C}

TeX:

{e}^{z} = \sum_{k=0}^{\infty} \frac{{z}^{k}}{k !}

z \in \mathbb{C}

Definitions:

Fungrim symbol	Notation	Short description
`Exp`	${e}^{z}$	Exponential function
`Sum`	$\sum_{n} f(n)$	Sum
`Pow`	${a}^{b}$	Power
`Factorial`	$n !$	Factorial
`Infinity`	$\infty$	Positive infinity
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("1635f5"),
    Formula(Equal(Exp(z), Sum(Div(Pow(z, k), Factorial(k)), For(k, 0, Infinity)))),
    Variables(z),
    Assumptions(Element(z, CC)))

65c610

{e}^{x + y} = \sum_{k=0}^{\infty} \sum_{n=0}^{\infty} {n + k \choose k} \frac{{x}^{k} {y}^{n}}{\left(n + k\right)!}

Assumptions:

x \in \mathbb{C} \;\mathbin{\operatorname{and}}\; y \in \mathbb{C}

TeX:

{e}^{x + y} = \sum_{k=0}^{\infty} \sum_{n=0}^{\infty} {n + k \choose k} \frac{{x}^{k} {y}^{n}}{\left(n + k\right)!}

x \in \mathbb{C} \;\mathbin{\operatorname{and}}\; y \in \mathbb{C}

Definitions:

Fungrim symbol	Notation	Short description
`Exp`	${e}^{z}$	Exponential function
`Sum`	$\sum_{n} f(n)$	Sum
`Binomial`	${n \choose k}$	Binomial coefficient
`Pow`	${a}^{b}$	Power
`Factorial`	$n !$	Factorial
`Infinity`	$\infty$	Positive infinity
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("65c610"),
    Formula(Equal(Exp(Add(x, y)), Sum(Sum(Mul(Binomial(Add(n, k), k), Div(Mul(Pow(x, k), Pow(y, n)), Factorial(Add(n, k)))), For(n, 0, Infinity)), For(k, 0, Infinity)))),
    Variables(x, y),
    Assumptions(And(Element(x, CC), Element(y, CC))))

50f57e

\sum_{n=0}^{\infty} {2 n \choose n} \frac{{x}^{n}}{n !} = {e}^{2 x} I_{0}\!\left(2 x\right)

Assumptions:

x \in \mathbb{C}

TeX:

\sum_{n=0}^{\infty} {2 n \choose n} \frac{{x}^{n}}{n !} = {e}^{2 x} I_{0}\!\left(2 x\right)

x \in \mathbb{C}

Definitions:

Fungrim symbol	Notation	Short description
`Sum`	$\sum_{n} f(n)$	Sum
`Binomial`	${n \choose k}$	Binomial coefficient
`Pow`	${a}^{b}$	Power
`Factorial`	$n !$	Factorial
`Infinity`	$\infty$	Positive infinity
`Exp`	${e}^{z}$	Exponential function
`BesselI`	$I_{\nu}\!\left(z\right)$	Modified Bessel function of the first kind
`CC`	$\mathbb{C}$	Complex numbers

Source code for this entry:

Entry(ID("50f57e"),
    Formula(Equal(Sum(Mul(Binomial(Mul(2, n), n), Div(Pow(x, n), Factorial(n))), For(n, 0, Infinity)), Mul(Exp(Mul(2, x)), BesselI(0, Mul(2, x))))),
    Variables(x),
    Assumptions(Element(x, CC)))

2b2066

\sum_{n=0}^{\infty} {2 n \choose n} {x}^{n} = \frac{1}{\sqrt{1 - 4 x}}

Assumptions:

x \in \mathbb{C} \;\mathbin{\operatorname{and}}\; \left|x\right| < \frac{1}{4}

TeX:

\sum_{n=0}^{\infty} {2 n \choose n} {x}^{n} = \frac{1}{\sqrt{1 - 4 x}}

x \in \mathbb{C} \;\mathbin{\operatorname{and}}\; \left|x\right| < \frac{1}{4}

Definitions:

Fungrim symbol	Notation	Short description
`Sum`	$\sum_{n} f(n)$	Sum
`Binomial`	${n \choose k}$	Binomial coefficient
`Pow`	${a}^{b}$	Power
`Infinity`	$\infty$	Positive infinity
`Sqrt`	$\sqrt{z}$	Principal square root
`CC`	$\mathbb{C}$	Complex numbers
`Abs`	$\left\|z\right\|$	Absolute value

Source code for this entry:

Entry(ID("2b2066"),
    Formula(Equal(Sum(Mul(Binomial(Mul(2, n), n), Pow(x, n)), For(n, 0, Infinity)), Div(1, Sqrt(Sub(1, Mul(4, x)))))),
    Variables(x),
    Assumptions(And(Element(x, CC), Less(Abs(x), Div(1, 4)))))

c9bcf7

\sum_{n=0}^{\infty} \frac{1}{{2 n \choose n}} {x}^{n} = \,{}_2F_1\!\left(1, 1, \frac{1}{2}, \frac{x}{4}\right) = \frac{1}{1 - u} + \frac{\sqrt{u} \operatorname{asin}\!\left(\sqrt{u}\right)}{{\left(1 - u\right)}^{3 / 2}}\; \text{ where } u = \frac{x}{4}

Assumptions:

x \in \mathbb{C} \;\mathbin{\operatorname{and}}\; \left|x\right| < 4

TeX:

\sum_{n=0}^{\infty} \frac{1}{{2 n \choose n}} {x}^{n} = \,{}_2F_1\!\left(1, 1, \frac{1}{2}, \frac{x}{4}\right) = \frac{1}{1 - u} + \frac{\sqrt{u} \operatorname{asin}\!\left(\sqrt{u}\right)}{{\left(1 - u\right)}^{3 / 2}}\; \text{ where } u = \frac{x}{4}

x \in \mathbb{C} \;\mathbin{\operatorname{and}}\; \left|x\right| < 4

Definitions:

Fungrim symbol	Notation	Short description
`Sum`	$\sum_{n} f(n)$	Sum
`Binomial`	${n \choose k}$	Binomial coefficient
`Pow`	${a}^{b}$	Power
`Infinity`	$\infty$	Positive infinity
`Hypergeometric2F1`	$\,{}_2F_1\!\left(a, b, c, z\right)$	Gauss hypergeometric function
`Sqrt`	$\sqrt{z}$	Principal square root
`CC`	$\mathbb{C}$	Complex numbers
`Abs`	$\left\|z\right\|$	Absolute value

Source code for this entry:

Entry(ID("c9bcf7"),
    Formula(Equal(Sum(Mul(Div(1, Binomial(Mul(2, n), n)), Pow(x, n)), For(n, 0, Infinity)), Hypergeometric2F1(1, 1, Div(1, 2), Div(x, 4)), Where(Add(Div(1, Sub(1, u)), Div(Mul(Sqrt(u), Asin(Sqrt(u))), Pow(Sub(1, u), Div(3, 2)))), Equal(u, Div(x, 4))))),
    Variables(x),
    Assumptions(And(Element(x, CC), Less(Abs(x), 4))))

bb8a75

n ! \le {n}^{n}

Assumptions:

n \in \mathbb{Z}_{\ge 0}

TeX:

n ! \le {n}^{n}

n \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Factorial`	$n !$	Factorial
`Pow`	${a}^{b}$	Power
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("bb8a75"),
    Formula(LessEqual(Factorial(n), Pow(n, n))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(0))))

f9efd0

n ! > {e}^{n}

Assumptions:

n \in \mathbb{Z}_{\ge 6}

TeX:

n ! > {e}^{n}

n \in \mathbb{Z}_{\ge 6}

Definitions:

Fungrim symbol	Notation	Short description
`Factorial`	$n !$	Factorial
`Exp`	${e}^{z}$	Exponential function
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("f9efd0"),
    Formula(Greater(Factorial(n), Exp(n))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(6))))

25b7bd

n ! > {C}^{n}

Assumptions:

n \in \mathbb{Z}_{\ge 1} \;\mathbin{\operatorname{and}}\; C \in \left(0, \infty\right) \;\mathbin{\operatorname{and}}\; n \ge C e

TeX:

n ! > {C}^{n}

n \in \mathbb{Z}_{\ge 1} \;\mathbin{\operatorname{and}}\; C \in \left(0, \infty\right) \;\mathbin{\operatorname{and}}\; n \ge C e

Definitions:

Fungrim symbol	Notation	Short description
`Factorial`	$n !$	Factorial
`Pow`	${a}^{b}$	Power
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`OpenInterval`	$\left(a, b\right)$	Open interval
`Infinity`	$\infty$	Positive infinity
`ConstE`	$e$	The constant e (2.718...)

Source code for this entry:

Entry(ID("25b7bd"),
    Formula(Greater(Factorial(n), Pow(C, n))),
    Variables(C, n),
    Assumptions(And(Element(n, ZZGreaterEqual(1)), Element(C, OpenInterval(0, Infinity)), GreaterEqual(n, Mul(C, ConstE)))))

6b3af0

{n \choose k} \le \frac{{n}^{k}}{k !}

Assumptions:

n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

{n \choose k} \le \frac{{n}^{k}}{k !}

n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Binomial`	${n \choose k}$	Binomial coefficient
`Pow`	${a}^{b}$	Power
`Factorial`	$n !$	Factorial
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("6b3af0"),
    Formula(LessEqual(Binomial(n, k), Div(Pow(n, k), Factorial(k)))),
    Variables(n, k),
    Assumptions(And(Element(n, ZZGreaterEqual(0)), Element(k, ZZGreaterEqual(0)))))

001a0b

{n \choose k} \ge \frac{{n}^{k}}{{k}^{k}}

Assumptions:

n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; k \in \{0, 1, \ldots, n\}

TeX:

{n \choose k} \ge \frac{{n}^{k}}{{k}^{k}}

n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; k \in \{0, 1, \ldots, n\}

Definitions:

Fungrim symbol	Notation	Short description
`Binomial`	${n \choose k}$	Binomial coefficient
`Pow`	${a}^{b}$	Power
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`Range`	$\{a, a + 1, \ldots, b\}$	Integers between given endpoints

Source code for this entry:

Entry(ID("001a0b"),
    Formula(GreaterEqual(Binomial(n, k), Div(Pow(n, k), Pow(k, k)))),
    Variables(n, k),
    Assumptions(And(Element(n, ZZGreaterEqual(0)), Element(k, Range(0, n)))))

5d6f99

{n \choose k} \le \frac{{\left(n e\right)}^{k}}{{k}^{k}}

Assumptions:

n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

{n \choose k} \le \frac{{\left(n e\right)}^{k}}{{k}^{k}}

n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Binomial`	${n \choose k}$	Binomial coefficient
`Pow`	${a}^{b}$	Power
`ConstE`	$e$	The constant e (2.718...)
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("5d6f99"),
    Formula(LessEqual(Binomial(n, k), Div(Pow(Mul(n, ConstE), k), Pow(k, k)))),
    Variables(n, k),
    Assumptions(And(Element(n, ZZGreaterEqual(0)), Element(k, ZZGreaterEqual(0)))))

4e7120

{n \choose k} \le \frac{{n}^{n}}{{k}^{k} {\left(n - k\right)}^{n - k}}

Assumptions:

n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; k \in \{0, 1, \ldots, n\}

TeX:

{n \choose k} \le \frac{{n}^{n}}{{k}^{k} {\left(n - k\right)}^{n - k}}

n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; k \in \{0, 1, \ldots, n\}

Definitions:

Fungrim symbol	Notation	Short description
`Binomial`	${n \choose k}$	Binomial coefficient
`Pow`	${a}^{b}$	Power
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`Range`	$\{a, a + 1, \ldots, b\}$	Integers between given endpoints

Source code for this entry:

Entry(ID("4e7120"),
    Formula(LessEqual(Binomial(n, k), Div(Pow(n, n), Mul(Pow(k, k), Pow(Sub(n, k), Sub(n, k)))))),
    Variables(n, k),
    Assumptions(And(Element(n, ZZGreaterEqual(0)), Element(k, Range(0, n)))))

fc8d5d

n ! < \sqrt{2 \pi} {n}^{n + 1 / 2} {e}^{-n} \exp\!\left(\frac{1}{12 n}\right)

Assumptions:

n \in \mathbb{Z}_{\ge 1}

References:

H. Robbins (1955), A remark on Stirling's formula, Am. Math. Monthly 62(1), pp. 26-29.

TeX:

n ! < \sqrt{2 \pi} {n}^{n + 1 / 2} {e}^{-n} \exp\!\left(\frac{1}{12 n}\right)

n \in \mathbb{Z}_{\ge 1}

Definitions:

Fungrim symbol	Notation	Short description
`Factorial`	$n !$	Factorial
`Sqrt`	$\sqrt{z}$	Principal square root
`Pi`	$\pi$	The constant pi (3.14...)
`Pow`	${a}^{b}$	Power
`Exp`	${e}^{z}$	Exponential function
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("fc8d5d"),
    Formula(Less(Factorial(n), Mul(Mul(Mul(Sqrt(Mul(2, Pi)), Pow(n, Add(n, Div(1, 2)))), Exp(Neg(n))), Exp(Div(1, Mul(12, n)))))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(1))),
    References("H. Robbins (1955), A remark on Stirling's formula, Am. Math. Monthly 62(1), pp. 26-29."))

1745f5

n ! > \sqrt{2 \pi} {n}^{n + 1 / 2} {e}^{-n} \exp\!\left(\frac{1}{12 n + 1}\right)

Assumptions:

n \in \mathbb{Z}_{\ge 0}

References:

H. Robbins (1955), A remark on Stirling's formula, Am. Math. Monthly 62(1), pp. 26-29.

TeX:

n ! > \sqrt{2 \pi} {n}^{n + 1 / 2} {e}^{-n} \exp\!\left(\frac{1}{12 n + 1}\right)

n \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Factorial`	$n !$	Factorial
`Sqrt`	$\sqrt{z}$	Principal square root
`Pi`	$\pi$	The constant pi (3.14...)
`Pow`	${a}^{b}$	Power
`Exp`	${e}^{z}$	Exponential function
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("1745f5"),
    Formula(Greater(Factorial(n), Mul(Mul(Mul(Sqrt(Mul(2, Pi)), Pow(n, Add(n, Div(1, 2)))), Exp(Neg(n))), Exp(Div(1, Add(Mul(12, n), 1)))))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(0))),
    References("H. Robbins (1955), A remark on Stirling's formula, Am. Math. Monthly 62(1), pp. 26-29."))

d3baaf

{n \choose k} < \frac{1}{\sqrt{2 \pi}} \sqrt{\frac{n}{k \left(n - k\right)}} \frac{{n}^{n}}{{k}^{k} {\left(n - k\right)}^{n - k}}

Assumptions:

n \in \mathbb{Z}_{\ge 2} \;\mathbin{\operatorname{and}}\; k \in \{1, 2, \ldots, n - 1\}

TeX:

{n \choose k} < \frac{1}{\sqrt{2 \pi}} \sqrt{\frac{n}{k \left(n - k\right)}} \frac{{n}^{n}}{{k}^{k} {\left(n - k\right)}^{n - k}}

n \in \mathbb{Z}_{\ge 2} \;\mathbin{\operatorname{and}}\; k \in \{1, 2, \ldots, n - 1\}

Definitions:

Fungrim symbol	Notation	Short description
`Binomial`	${n \choose k}$	Binomial coefficient
`Sqrt`	$\sqrt{z}$	Principal square root
`Pi`	$\pi$	The constant pi (3.14...)
`Pow`	${a}^{b}$	Power
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`Range`	$\{a, a + 1, \ldots, b\}$	Integers between given endpoints

Source code for this entry:

Entry(ID("d3baaf"),
    Formula(Less(Binomial(n, k), Mul(Mul(Div(1, Sqrt(Mul(2, Pi))), Sqrt(Div(n, Mul(k, Sub(n, k))))), Div(Pow(n, n), Mul(Pow(k, k), Pow(Sub(n, k), Sub(n, k))))))),
    Variables(n, k),
    Assumptions(And(Element(n, ZZGreaterEqual(2)), Element(k, Range(1, Sub(n, 1))))))

5f7334

{n \choose k} \ge \frac{1}{\sqrt{8}} \sqrt{\frac{n}{k \left(n - k\right)}} \frac{{n}^{n}}{{k}^{k} {\left(n - k\right)}^{n - k}}

Assumptions:

n \in \mathbb{Z}_{\ge 2} \;\mathbin{\operatorname{and}}\; k \in \{1, 2, \ldots, n - 1\}

TeX:

{n \choose k} \ge \frac{1}{\sqrt{8}} \sqrt{\frac{n}{k \left(n - k\right)}} \frac{{n}^{n}}{{k}^{k} {\left(n - k\right)}^{n - k}}

n \in \mathbb{Z}_{\ge 2} \;\mathbin{\operatorname{and}}\; k \in \{1, 2, \ldots, n - 1\}

Definitions:

Fungrim symbol	Notation	Short description
`Binomial`	${n \choose k}$	Binomial coefficient
`Sqrt`	$\sqrt{z}$	Principal square root
`Pow`	${a}^{b}$	Power
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`Range`	$\{a, a + 1, \ldots, b\}$	Integers between given endpoints

Source code for this entry:

Entry(ID("5f7334"),
    Formula(GreaterEqual(Binomial(n, k), Mul(Mul(Div(1, Sqrt(8)), Sqrt(Div(n, Mul(k, Sub(n, k))))), Div(Pow(n, n), Mul(Pow(k, k), Pow(Sub(n, k), Sub(n, k))))))),
    Variables(n, k),
    Assumptions(And(Element(n, ZZGreaterEqual(2)), Element(k, Range(1, Sub(n, 1))))))

433d8b

{2 n \choose n} < \frac{{4}^{n}}{\sqrt{\pi n}}

Assumptions:

n \in \mathbb{Z}_{\ge 1}

TeX:

{2 n \choose n} < \frac{{4}^{n}}{\sqrt{\pi n}}

n \in \mathbb{Z}_{\ge 1}

Definitions:

Fungrim symbol	Notation	Short description
`Binomial`	${n \choose k}$	Binomial coefficient
`Pow`	${a}^{b}$	Power
`Sqrt`	$\sqrt{z}$	Principal square root
`Pi`	$\pi$	The constant pi (3.14...)
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("433d8b"),
    Formula(Less(Binomial(Mul(2, n), n), Div(Pow(4, n), Sqrt(Mul(Pi, n))))),
    Variables(n),
    Assumptions(Element(n, ZZGreaterEqual(1))))

fa3b53

{n \choose k} \le {2}^{n}

Assumptions:

n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

TeX:

{n \choose k} \le {2}^{n}

n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; k \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Binomial`	${n \choose k}$	Binomial coefficient
`Pow`	${a}^{b}$	Power
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("fa3b53"),
    Formula(LessEqual(Binomial(n, k), Pow(2, n))),
    Variables(n, k),
    Assumptions(And(Element(n, ZZGreaterEqual(0)), Element(k, ZZGreaterEqual(0)))))

Specific values

Product representations

Functional equations and recurrence relations

Connection formulas

Sums and generating functions

Bounds and inequalities