Square root on RCLike

This file contains the definitions Complex.sqrt and RCLike.sqrt and builds basic API.

noncomputable def Complex.sqrt (a : ℂ) : ℂ

The square root of a complex number.

@[simp]

theorem Complex.sqrt_zero : sqrt 0 = 0

@[simp]

theorem Complex.sqrt_one : sqrt 1 = 1

theorem Complex.sqrt_eq_real_add_ite {a : ℂ} : a.sqrt = ↑√((‖a‖ + a.re) / 2) + (if 0 ≤ a.im then 1 else -1) * ↑√((‖a‖ - a.re) / 2) * I

noncomputable def RCLike.sqrt {𝕜 : Type u_1} [RCLike 𝕜] (a : 𝕜) : 𝕜

The square root on RCLike.

theorem RCLike.sqrt_eq_ite {𝕜 : Type u_1} [RCLike 𝕜] {a : 𝕜} : sqrt a = if h : im I = 1 then (complexRingEquiv h).symm ((complexRingEquiv h) a).sqrt else ↑√(re a)

theorem RCLike.sqrt_eq_real_add_ite {𝕜 : Type u_1} [RCLike 𝕜] {a : 𝕜} : sqrt a = ↑√((‖a‖ + re a) / 2) + (if 0 ≤ im a then 1 else -1) * ↑√((‖a‖ - re a) / 2) * I

@[simp]

theorem RCLike.sqrt_zero {𝕜 : Type u_1} [RCLike 𝕜] : sqrt 0 = 0

@[simp]

theorem RCLike.sqrt_one {𝕜 : Type u_1} [RCLike 𝕜] : sqrt 1 = 1

theorem Complex.re_sqrt_ofReal {a : ℝ} : (↑a).sqrt.re = √a

theorem RCLike.re_sqrt_ofReal {𝕜 : Type u_1} [RCLike 𝕜] {a : ℝ} : re (sqrt ↑a) = √a

@[simp]

theorem RCLike.sqrt_real {a : ℝ} : sqrt a = √a

@[simp]

theorem RCLike.sqrt_complex {a : ℂ} : sqrt a = a.sqrt

theorem Complex.sqrt_of_nonneg {a : ℂ} (ha : 0 ≤ a) : a.sqrt = ↑√a.re

theorem RCLike.sqrt_map {𝕜 : Type u_1} [RCLike 𝕜] {𝕜' : Type u_2} [RCLike 𝕜'] {a : 𝕜} (h : im I = im I) : sqrt ((map 𝕜 𝕜') a) = (map 𝕜 𝕜') (sqrt a)

theorem Complex.sqrt_map {𝕜 : Type u_1} [RCLike 𝕜] {a : 𝕜} (h : RCLike.im RCLike.I = 1) : ((RCLike.map 𝕜 ℂ) a).sqrt = (RCLike.map 𝕜 ℂ) (RCLike.sqrt a)

theorem RCLike.sqrt_of_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {a : 𝕜} (ha : 0 ≤ a) : sqrt a = ↑√(re a)

theorem Complex.sqrt_neg_of_nonneg {a : ℂ} (ha : 0 ≤ a) : (-a).sqrt = I * a.sqrt

theorem RCLike.sqrt_neg_of_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {a : 𝕜} (ha : 0 ≤ a) : sqrt (-a) = I * sqrt a

theorem Complex.sqrt_neg_one : (-1).sqrt = I

theorem RCLike.sqrt_neg_one {𝕜 : Type u_1} [RCLike 𝕜] : sqrt (-1) = I

theorem Complex.sqrt_I : I.sqrt = ↑√2⁻¹ * (1 + I)

theorem Complex.sqrt_neg_I : (-I).sqrt = ↑√2⁻¹ * (1 - I)

theorem RCLike.sqrt_I {𝕜 : Type u_1} [RCLike 𝕜] : sqrt I = ↑√2⁻¹ * (1 - I) * I

theorem RCLike.sqrt_neg_I {𝕜 : Type u_1} [RCLike 𝕜] : sqrt (-I) = ↑√2⁻¹ * (1 + I) * -I