Documentation

Mathlib.Analysis.RCLike.Sqrt

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.

Equations

a.sqrt = a ^ 2⁻¹

Instances For

@[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.

Equations

RCLike.sqrt a = (RCLike.map ℂ 𝕜) ((RCLike.map 𝕜 ℂ) a).sqrt

Instances For

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 : ℝ} :

@[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