Csqrt

noncomputable def csqrt : ℂ → ℂ

The principal complex square root a ↦ exp ((1 / 2) * log a).

Equations

• csqrt a = Complex.exp (1 / 2 * Complex.log a)

theorem csqrt_deriv (z : UpperHalfPlane) : deriv (fun (a : ℂ) => Complex.exp (1 / 2 * Complex.log a)) ↑z = 2⁻¹ • (fun (a : ℂ) => Complex.exp (-(1 / 2) * Complex.log a)) ↑z

theorem csqrt_differentiableAt (z : UpperHalfPlane) : DifferentiableAt ℂ csqrt ↑z

theorem csqrt_I : csqrt Complex.I ^ 24 = 1

theorem csqrt_pow_24 (z : ℂ) (hz : z ≠ 0) : csqrt z ^ 24 = z ^ 12