The principal square root and the slit plane

The principal square root has nonnegative real part, and its real part is strictly positive exactly on the slit plane. These facts control the branches in algebraic transformations involving sums of principal roots.

@[simp]

theorem Complex.sq_sqrt (z : ℂ) : z.sqrt ^ 2 = z

The square of the principal square root is the original complex number.

@[simp]

theorem Complex.sqrt_re_nonneg (z : ℂ) : 0 ≤ z.sqrt.re

The principal square root has nonnegative real part.

theorem Complex.sqrt_im_nonneg {z : ℂ} (h : 0 ≤ z.im) : 0 ≤ z.sqrt.im

The principal square root has nonnegative imaginary part when the input does.

@[simp]

theorem Complex.sqrt_re_pos_iff (z : ℂ) : 0 < z.sqrt.re ↔ z ∈ slitPlane

The principal square root has positive real part exactly on the slit plane.

@[simp]

theorem Complex.sqrt_add_sqrt_re_pos_iff (x y : ℂ) : 0 < x.sqrt.re + y.sqrt.re ↔ x ∈ slitPlane ∨ y ∈ slitPlane

A sum of principal square roots has positive real part exactly when at least one input lies in the slit plane.