Assumptions:
TeX:
\frac{d^{r}}{{d z}^{r}} \sqrt{z} = {\left(-1\right)}^{r} \left(-\frac{1}{2}\right)_{r} {z}^{r - 1 / 2}
z \in \mathbb{C} \setminus \left(-\infty, 0\right] \;\mathbin{\operatorname{and}}\; r \in \mathbb{Z}_{\ge 0}Definitions:
| Fungrim symbol | Notation | Short description |
|---|---|---|
| ComplexDerivative | Complex derivative | |
| Sqrt | Principal square root | |
| Pow | Power | |
| RisingFactorial | Rising factorial | |
| CC | Complex numbers | |
| OpenClosedInterval | Open-closed interval | |
| Infinity | Positive infinity | |
| ZZGreaterEqual | Integers greater than or equal to n |
Source code for this entry:
Entry(ID("83abff"),
Formula(Equal(ComplexDerivative(Sqrt(z), For(z, z, r)), Mul(Mul(Pow(-1, r), RisingFactorial(Neg(Div(1, 2)), r)), Pow(z, Sub(r, Div(1, 2)))))),
Variables(z, r),
Assumptions(And(Element(z, SetMinus(CC, OpenClosedInterval(Neg(Infinity), 0))), Element(r, ZZGreaterEqual(0)))))