Revision #1212 → #1826 · back to history
modifiedFactorial (informal)4f9f03b7705a
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"(Lead)","snippet":"the factorial of a non-negative integer"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}n!&=n\\times (n-1)\\times (n-2)\\times (n-3)\\times \\cdots \\times 3\\times 2\\times 1\\\\&={\\begin{cases}1,&{\\text{if }}n=0\\\\n\\times (n-1)!,&{\\text{if }}n\\geq 1.\\end{cases}}\\\\\\end{aligned}}}"},{"type":"math_alttext","value":"{\\displaystyle 5!=5\\times 4!=5\\times 4\\times 3\\times 2\\times 1=120.}"}] | — |
modifiedZero factorial conventiondec467631c4d
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"(Lead)","snippet":"The value of 0! is 1"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}n!&=n\\times (n-1)\\times (n-2)\\times (n-3)\\times \\cdots \\times 3\\times 2\\times 1\\\\&={\\begin{cases}1,&{\\text{if }}n=0\\\\n\\times (n-1)!,&{\\text{if }}n\\geq 1.\\end{cases}}\\\\\\end{aligned}}}"},{"type":"math_alttext","value":"{\\displaystyle 5!=5\\times 4!=5\\times 4\\times 3\\times 2\\times 1=120.}"}] | — |
modifiedFactorial function947a264ba769
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Definition","snippet":"The factorial function of a positive integer"},{"type":"math_alttext","value":"{\\displaystyle n!=1\\cdot 2\\cdot 3\\cdots (n-2)\\cdot (n-1)\\cdot n.}"},{"type":"math_alttext","value":"{\\displaystyle n!=\\prod _{i=1}^{n}i.}"}] | — |
modifiedFactorial recurrence relationd19a4700ed3c
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Definition","snippet":"This leads to a recurrence relation"},{"type":"math_alttext","value":"{\\displaystyle n!=n\\cdot (n-1)!.}"}] | — |
modifiedCounting permutationsc46af0af9b4f
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Applications","snippet":"different ways of arranging"},{"type":"math_alttext","value":"{\\displaystyle {\\binom {n}{k}}={\\frac {n!}{k!(n-k)!}}.}"}] | — |
modifiedBinomial coefficients via factorialsca1bf2f122b9
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Applications","snippet":"For instance the binomial coefficients"},{"type":"math_alttext","value":"{\\displaystyle {\\binom {n}{k}}={\\frac {n!}{k!(n-k)!}}.}"}] | — |
modifiedStirling numbers of the first kind sum to factorialscac93bd77a75
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Applications","snippet":"The Stirling numbers of the first kind sum to the factorials"},{"type":"math_alttext","value":"{\\displaystyle {\\binom {n}{k}}={\\frac {n!}{k!(n-k)!}}.}"}] | — |
modifiedCounting derangements549d9e967c78
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Applications","snippet":"Another combinatorial application is in counting derangements"},{"type":"math_alttext","value":"{\\displaystyle {\\binom {n}{k}}={\\frac {n!}{k!(n-k)!}}.}"}] | — |
modifiedFactorials are orders of symmetric groups424e5204d70c
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Applications","snippet":"the factorials are the orders of finite symmetric groups"},{"type":"math_alttext","value":"{\\displaystyle e^{x}=1+{\\frac {x}{1}}+{\\frac {x^{2}}{2}}+{\\frac {x^{3}}{6}}+\\cdots =\\sum _{k=0}^{\\infty }{\\frac {x^{k}}{k!}},}"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{k=0}^{\\infty }{\\frac {x^{k}n_{k}}{k!}}.}"}] | — |
modifiedExponential generating function23806efeba38
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Applications","snippet":"the exponential generating function"},{"type":"math_alttext","value":"{\\displaystyle e^{x}=1+{\\frac {x}{1}}+{\\frac {x^{2}}{2}}+{\\frac {x^{3}}{6}}+\\cdots =\\sum _{k=0}^{\\infty }{\\frac {x^{k}}{k!}},}"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{k=0}^{\\infty }{\\frac {x^{k}n_{k}}{k!}}.}"}] | — |
modifiedEuclid's theorem (infinitude of primes)028189033791
| Field | From #1212 | To #1826 |
|---|
| mathlib.module | Mathlib.Data.Nat.Prime.Basic | Mathlib.Data.Nat.Prime.Infinite |
modifiedGrowth rate of factorial9876e333448e
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Growth and approximation","snippet":"the factorial has faster than exponential growth"},{"type":"math_alttext","value":"{\\displaystyle \\ln n!=\\sum _{x=1}^{n}\\ln x\\approx \\int _{1}^{n}\\ln x\\,dx=n\\ln n-n+1.}"},{"type":"math_alttext","value":"{\\displaystyle n!\\sim {\\sqrt {2\\pi n}}\\left({\\frac {n}{e}}\\right)^{n}\\,.}"},{"type":"math_alttext","value":"{\\displaystyle n!\\sim {\\sqrt {2\\pi n}}\\left({\\frac {n}{e}}\\right)^{n}\\left(1+{\\frac {1}{12n}}+{\\frac {1}{288n^{2}}}-{\\frac {139}{51840n^{3}}}-{\\frac {571}{2488320n^{4}}}+\\cdots \\right).}"},{"type":"math_alttext","value":"{\\displaystyle n!\\sim {\\sqrt {2\\pi n}}\\left({\\frac {n}{e}}\\right)^{n}\\exp \\left({\\frac {1}{12n}}-{\\frac {1}{360n^{3}}}+{\\frac {1}{1260n^{5}}}-{\\frac {1}{1680n^{7}}}+\\cdots \\right).}"}] | — |
modifiedStirling's approximation182e62d69741
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Growth and approximation","snippet":"The result of these corrections is Stirling's approximation"},{"type":"math_alttext","value":"{\\displaystyle \\ln n!=\\sum _{x=1}^{n}\\ln x\\approx \\int _{1}^{n}\\ln x\\,dx=n\\ln n-n+1.}"},{"type":"math_alttext","value":"{\\displaystyle n!\\sim {\\sqrt {2\\pi n}}\\left({\\frac {n}{e}}\\right)^{n}\\,.}"},{"type":"math_alttext","value":"{\\displaystyle n!\\sim {\\sqrt {2\\pi n}}\\left({\\frac {n}{e}}\\right)^{n}\\left(1+{\\frac {1}{12n}}+{\\frac {1}{288n^{2}}}-{\\frac {139}{51840n^{3}}}-{\\frac {571}{2488320n^{4}}}+\\cdots \\right).}"},{"type":"math_alttext","value":"{\\displaystyle n!\\sim {\\sqrt {2\\pi n}}\\left({\\frac {n}{e}}\\right)^{n}\\exp \\left({\\frac {1}{12n}}-{\\frac {1}{360n^{3}}}+{\\frac {1}{1260n^{5}}}-{\\frac {1}{1680n^{7}}}+\\cdots \\right).}"}] | — |
modifiedBinary logarithm of the factorial643f08874f1a
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Growth and approximation","snippet":"The binary logarithm of the factorial"},{"type":"math_alttext","value":"{\\displaystyle \\log _{2}n!=n\\log _{2}n-n\\log _{2}e+{\\frac {1}{2}}\\log _{2}n+O(1).}"}] | — |
modifiedDivisibility of n! by primes up to nca9767e4c3d7
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Divisibility and digits","snippet":"is divisible by all prime numbers that are at most"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{i=1}^{\\infty }\\left\\lfloor {\\frac {n}{p^{i}}}\\right\\rfloor ={\\frac {n-s_{p}(n)}{p-1}}.}"}] | — |
modifiedLegendre's formula336707de7eb4
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Divisibility and digits","snippet":"More precise information about its divisibility is given by Legendre's formula"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{i=1}^{\\infty }\\left\\lfloor {\\frac {n}{p^{i}}}\\right\\rfloor ={\\frac {n-s_{p}(n)}{p-1}}.}"}] | — |
modifiedKummer's theorem3ab07522bac8
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Divisibility and digits","snippet":"produces Kummer's theorem"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{i=1}^{\\infty }\\left\\lfloor {\\frac {n}{p^{i}}}\\right\\rfloor ={\\frac {n-s_{p}(n)}{p-1}}.}"}] | — |
modifiedGamma function (integral definition)18b452f88e7c
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Continuous interpolation and non-integer generalization","snippet":"which can be defined for positive real numbers as the integral"},{"type":"math_alttext","value":"{\\displaystyle \\Gamma (z)=\\int _{0}^{\\infty }x^{z-1}e^{-x}\\,dx.}"},{"type":"math_alttext","value":"{\\displaystyle n!=\\Gamma (n+1),}"},{"type":"math_alttext","value":"{\\displaystyle \\Gamma (n)=(n-1)\\Gamma (n-1),}"}] | — |
modifiedGamma function functional equation0b1d42945fbd
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Continuous interpolation and non-integer generalization","snippet":"the gamma function obeys the functional equation"},{"type":"math_alttext","value":"{\\displaystyle \\Gamma (z)=\\int _{0}^{\\infty }x^{z-1}e^{-x}\\,dx.}"},{"type":"math_alttext","value":"{\\displaystyle n!=\\Gamma (n+1),}"},{"type":"math_alttext","value":"{\\displaystyle \\Gamma (n)=(n-1)\\Gamma (n-1),}"}] | — |
modifiedEuler's reflection formula7defb3e595c1
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Continuous interpolation and non-integer generalization","snippet":"Euler's reflection formula"},{"type":"math_alttext","value":"{\\displaystyle \\Gamma (z)\\Gamma (1-z)={\\frac {\\pi }{\\sin \\pi z}}.}"}] | — |
modifiedMeromorphic continuation of gamma functionb1fc14b99e14
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Continuous interpolation and non-integer generalization","snippet":"The result of this extension process is an analytic function"},{"type":"math_alttext","value":"{\\displaystyle \\Gamma (z)\\Gamma (1-z)={\\frac {\\pi }{\\sin \\pi z}}.}"}] | — |
modifiedWielandt's uniqueness theorem05061bad6ce1
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Continuous interpolation and non-integer generalization","snippet":"A related uniqueness theorem of Helmut Wielandt"},{"type":"math_alttext","value":"{\\displaystyle \\Gamma (z)\\Gamma (1-z)={\\frac {\\pi }{\\sin \\pi z}}.}"}] | — |
modifiedAlternating factorialce3ce6da7894
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Related sequences and functions","snippet":"The alternating factorial is the absolute value of the alternating sum"},{"type":"math_alttext","value":"{\\displaystyle (2k-1)!!=\\prod _{i=1}^{k}(2i-1)={\\frac {(2k)!}{2^{k}k!}}.}"},{"type":"math_alttext","value":"{\\displaystyle 4^{3^{2^{1}}}=262144.}"}] | — |
modifiedBhargava factorialsd3442659cd5a
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Related sequences and functions","snippet":"The Bhargava factorials are a family of integer sequences"},{"type":"math_alttext","value":"{\\displaystyle (2k-1)!!=\\prod _{i=1}^{k}(2i-1)={\\frac {(2k)!}{2^{k}k!}}.}"},{"type":"math_alttext","value":"{\\displaystyle 4^{3^{2^{1}}}=262144.}"}] | — |
modifiedDouble factorial0012ae7a3bbf
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Related sequences and functions","snippet":"is called the double factorial of"},{"type":"math_alttext","value":"{\\displaystyle (2k-1)!!=\\prod _{i=1}^{k}(2i-1)={\\frac {(2k)!}{2^{k}k!}}.}"},{"type":"math_alttext","value":"{\\displaystyle 4^{3^{2^{1}}}=262144.}"}] | — |
modifiedDouble factorial of 9ed176bda1213
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Related sequences and functions","snippet":"For example, 9!! = 1 × 3 × 5 × 7 × 9 = 945"},{"type":"math_alttext","value":"{\\displaystyle (2k-1)!!=\\prod _{i=1}^{k}(2i-1)={\\frac {(2k)!}{2^{k}k!}}.}"},{"type":"math_alttext","value":"{\\displaystyle 4^{3^{2^{1}}}=262144.}"}] | — |
modifiedExponential factorialc69b9e5c718e
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Related sequences and functions","snippet":"The exponential factorial is defined recursively"},{"type":"math_alttext","value":"{\\displaystyle (2k-1)!!=\\prod _{i=1}^{k}(2i-1)={\\frac {(2k)!}{2^{k}k!}}.}"},{"type":"math_alttext","value":"{\\displaystyle 4^{3^{2^{1}}}=262144.}"}] | — |
modifiedFalling factorialfd8f7c84045a
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Related sequences and functions","snippet":"This is also known as a falling factorial"},{"type":"math_alttext","value":"{\\displaystyle (2k-1)!!=\\prod _{i=1}^{k}(2i-1)={\\frac {(2k)!}{2^{k}k!}}.}"},{"type":"math_alttext","value":"{\\displaystyle 4^{3^{2^{1}}}=262144.}"}] | — |
modifiedHyperfactorialf269c701e2b8
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Related sequences and functions","snippet":"The hyperfactorial of"},{"type":"math_alttext","value":"{\\displaystyle (2k-1)!!=\\prod _{i=1}^{k}(2i-1)={\\frac {(2k)!}{2^{k}k!}}.}"},{"type":"math_alttext","value":"{\\displaystyle 4^{3^{2^{1}}}=262144.}"}] | — |
modifiedJordan–Pólya numbersbd54c42c033f
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Related sequences and functions","snippet":"The Jordan–Pólya numbers are the products of factorials"},{"type":"math_alttext","value":"{\\displaystyle (2k-1)!!=\\prod _{i=1}^{k}(2i-1)={\\frac {(2k)!}{2^{k}k!}}.}"},{"type":"math_alttext","value":"{\\displaystyle 4^{3^{2^{1}}}=262144.}"}] | — |
modifiedPrimorialc8e612e9886f
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Related sequences and functions","snippet":"is the product of prime numbers less than or equal to"},{"type":"math_alttext","value":"{\\displaystyle (2k-1)!!=\\prod _{i=1}^{k}(2i-1)={\\frac {(2k)!}{2^{k}k!}}.}"},{"type":"math_alttext","value":"{\\displaystyle 4^{3^{2^{1}}}=262144.}"}] | — |
modifiedSubfactoriald2637d1c6e1a
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Related sequences and functions","snippet":"The subfactorial yields the number of derangements"},{"type":"math_alttext","value":"{\\displaystyle (2k-1)!!=\\prod _{i=1}^{k}(2i-1)={\\frac {(2k)!}{2^{k}k!}}.}"},{"type":"math_alttext","value":"{\\displaystyle 4^{3^{2^{1}}}=262144.}"}] | — |
modifiedSuperfactorial4b03ccce8e5a
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Related sequences and functions","snippet":"The superfactorial of"},{"type":"math_alttext","value":"{\\displaystyle (2k-1)!!=\\prod _{i=1}^{k}(2i-1)={\\frac {(2k)!}{2^{k}k!}}.}"},{"type":"math_alttext","value":"{\\displaystyle 4^{3^{2^{1}}}=262144.}"}] | — |
modifiedTermial (triangular number)875a39a0b40e
| Field | From #1212 | To #1826 |
|---|
| anchors | [{"section":"Related sequences and functions","snippet":"Donald Knuth has proposed the name termial"},{"type":"math_alttext","value":"{\\displaystyle (2k-1)!!=\\prod _{i=1}^{k}(2i-1)={\\frac {(2k)!}{2^{k}k!}}.}"},{"type":"math_alttext","value":"{\\displaystyle 4^{3^{2^{1}}}=262144.}"}] | — |
addedExponential power series841a7ee6c677
addedBinomial theorem6279bd1f7fdc
addedFaà di Bruno's formula3417c1791895
addedWallis product33c5d3538c0b
addedPochhammer symbol9ad5e11a147f
addedFalling factorial as descending producte402b59cd85a
addedBarnes G-function6edabb019db8
addedK-functionc0092d3127b9
addedHermite polynomial discriminants are hyperfactorialsb4b0c6a5fe52
addedPoisson distribution uses factorialsf89856218713