Assumptions:
TeX:
{x}^{n} = \sum_{k=0}^{n} \left\{{n \atop k}\right\} \left(x - n + 1\right)_{n}
n \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; x \in \mathbb{C}Definitions:
| Fungrim symbol | Notation | Short description | 
|---|---|---|
| Pow | Power | |
| Sum | Sum | |
| StirlingS2 | Stirling number of the second kind | |
| RisingFactorial | Rising factorial | |
| ZZGreaterEqual | Integers greater than or equal to n | |
| CC | Complex numbers | 
Source code for this entry:
Entry(ID("b823b0"),
    Formula(Equal(Pow(x, n), Sum(Mul(StirlingS2(n, k), RisingFactorial(Add(Sub(x, n), 1), n)), For(k, 0, n)))),
    Variables(x, n),
    Assumptions(And(Element(n, ZZGreaterEqual(0)), Element(x, CC))))