# Fungrim entry: 21d9b8

Symbol: Sqrt $\sqrt{z}$ Principal square root
The principal square root $\sqrt{z}$ is a function of one complex variable $z$.
It has a branch point singularity at $z = 0$ and a branch cut on $\left(-\infty, 0\right]$ where the value on $\left(-\infty, 0\right)$ is taken to be continuous with the upper half plane.
The following table lists all conditions such that Sqrt(z) is defined in Fungrim.
Domain Codomain
Numbers
$z \in \left[0, \infty\right)$ $\sqrt{z} \in \left[0, \infty\right)$
$z \in \mathbb{C}$ $\sqrt{z} \in \mathbb{C}$
Infinities
$z \in \left\{{\tilde \infty}\right\}$ $\sqrt{z} \in \left\{{\tilde \infty}\right\}$
$z \in \left\{ {e}^{i \theta} \infty : \theta \in \left(-\pi, \pi\right] \right\}$ $\sqrt{z} \in \left\{ {e}^{i \theta} \infty : \theta \in \left(\frac{-\pi}{2}, \frac{\pi}{2}\right] \right\}$
Formal power series
$z \in \mathbb{R}[[x]] \,\mathbin{\operatorname{and}}\, [{x}^{0}] z \in \left(0, \infty\right)$ $\sqrt{z} \in \mathbb{R}[[x]]$
$z \in \mathbb{C}[[x]] \,\mathbin{\operatorname{and}}\, [{x}^{0}] z \ne 0$ $\sqrt{z} \in \mathbb{C}[[x]]$
Table data: $\left(P, Q\right)$ such that $\left(P\right) \implies \left(Q\right)$
Definitions:
Fungrim symbol Notation Short description
Sqrt$\sqrt{z}$ Principal square root
OpenClosedInterval$\left(a, b\right]$ Open-closed interval
Infinity$\infty$ Positive infinity
OpenInterval$\left(a, b\right)$ Open interval
ClosedOpenInterval$\left[a, b\right)$ Closed-open interval
CC$\mathbb{C}$ Complex numbers
UnsignedInfinity${\tilde \infty}$ Unsigned infinity
SetBuilder$\left\{ f\!\left(x\right) : P\!\left(x\right) \right\}$ Set comprehension
Exp${e}^{z}$ Exponential function
ConstI$i$ Imaginary unit
ConstPi$\pi$ The constant pi (3.14...)
FormalPowerSeries$K[[x]]$ Formal power series
RR$\mathbb{R}$ Real numbers
Source code for this entry:
Entry(ID("21d9b8"),
SymbolDefinition(Sqrt, Sqrt(z), "Principal square root"),
Description("The principal square root", Sqrt(z), "is a function of one complex variable", z, "."),
Description("It has a branch point singularity at", Equal(z, 0), "and a branch cut on", OpenClosedInterval(Neg(Infinity), 0), "where the value on", OpenInterval(Neg(Infinity), 0), "is taken to be continuous with the upper half plane."),
Description("The following table lists all conditions such that", SourceForm(Sqrt(z)), "is defined in Fungrim."),
Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(TableSection("Numbers"), Tuple(Element(z, ClosedOpenInterval(0, Infinity)), Element(Sqrt(z), ClosedOpenInterval(0, Infinity))), Tuple(Element(z, CC), Element(Sqrt(z), CC)), TableSection("Infinities"), Tuple(Element(z, Set(UnsignedInfinity)), Element(Sqrt(z), Set(UnsignedInfinity))), Tuple(Element(z, SetBuilder(Mul(Exp(Mul(ConstI, theta)), Infinity), theta, Element(theta, OpenClosedInterval(Neg(ConstPi), ConstPi)))), Element(Sqrt(z), SetBuilder(Mul(Exp(Mul(ConstI, theta)), Infinity), theta, Element(theta, OpenClosedInterval(Div(Neg(ConstPi), 2), Div(ConstPi, 2)))))), TableSection("Formal power series"), Tuple(And(Element(z, FormalPowerSeries(RR, x)), Element(SeriesCoefficient(z, x, 0), OpenInterval(0, Infinity))), And(Element(Sqrt(z), FormalPowerSeries(RR, x)))), Tuple(And(Element(z, FormalPowerSeries(CC, x)), Unequal(SeriesCoefficient(z, x, 0), 0)), And(Element(Sqrt(z), FormalPowerSeries(CC, x)))))))

## Topics using this entry

Copyright (C) Fredrik Johansson and contributors. Fungrim is provided under the MIT license. The source code is on GitHub.

2019-08-21 11:44:15.926409 UTC