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
    Instances For
      noncomputable def RCLike.sqrt {๐•œ : Type u_1} [RCLike ๐•œ] (a : ๐•œ) :
      ๐•œ

      The square root on RCLike.

      Equations
        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 RCLike.re_sqrt_ofReal {๐•œ : Type u_1} [RCLike ๐•œ] {a : โ„} :
          re (sqrt โ†‘a) = โˆša
          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 RCLike.sqrt_neg_of_nonneg {๐•œ : Type u_1} [RCLike ๐•œ] {a : ๐•œ} (ha : 0 โ‰ค a) :
          sqrt (-a) = I * sqrt a
          theorem RCLike.sqrt_neg_one {๐•œ : Type u_1} [RCLike ๐•œ] :
          sqrt (-1) = I
          theorem RCLike.sqrt_I {๐•œ : Type u_1} [RCLike ๐•œ] :
          theorem RCLike.sqrt_neg_I {๐•œ : Type u_1} [RCLike ๐•œ] :