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

Equations

• x.sqrt = x ^ 2⁻¹

def Complex.«term√_» : Lean.ParserDescr

Equations

• Complex.«term√_» = Lean.ParserDescr.node `Complex.«term√_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "√") (Lean.ParserDescr.cat `term 1024))

def Complex.nnr (x : ℂ) : Prop

Equations

• x.nnr = (0 ≤ x.re ∧ x.im = 0)

@[simp]

theorem Complex.norm_mk {a b : ℝ} : ‖{ re := a, im := b }‖ = √(a ^ 2 + b ^ 2)

theorem Complex.sqrt_eq_iff_eq_sq_of_nnr {a b : ℂ} (h₁ : a.nnr) (h₂ : b.nnr) : a.sqrt = b ↔ a = b ^ 2

theorem Complex.sqrt_re_of_nnr {a : ℂ} (h : a.nnr) : a.sqrt.re = √|a.re|

theorem Complex.sqrt_im_of_nnr {a : ℂ} (h : a.nnr) : a.sqrt.im = 0

theorem Complex.ofNat_eq {n : ℕ} : OfNat.ofNat n = ↑n

@[simp]

theorem Complex.nnr_nat {n : ℕ} : (OfNat.ofNat n).nnr

@[simp]

theorem Complex.nnr_natCast {n : ℕ} : (↑n).nnr

@[simp]

theorem Complex.sqrt_nat_re {n : ℕ} : (OfNat.ofNat n).sqrt.re = √(OfNat.ofNat n)

@[simp]

theorem Complex.sqrt_nat_im {n : ℕ} : (OfNat.ofNat n).sqrt.im = 0

theorem Complex.eq_of_re_eq_re {a b : ℂ} (h₁ : a.im = 0) (h₂ : b.im = 0) (h₃ : a.re = b.re) : a = b

@[simp]

theorem Complex.sq_sqrt {a : ℂ} : a.sqrt ^ 2 = a

theorem Complex.nnr_of_sqrt_im_eq_zero {x : ℂ} (h : x.sqrt.im = 0) : x.nnr

theorem Complex.sqrt_im_eq_zero_iff {x : ℂ} : x.sqrt.im = 0 ↔ x.nnr

theorem Complex.nnr_add {a b : ℂ} (ha : a.nnr) (hb : b.nnr) : (a + b).nnr

theorem Complex.nnr_mul {a b : ℂ} (ha : a.nnr) (hb : b.nnr) : (a * b).nnr

theorem Complex.sqrt_mul_of_nnr {a b : ℂ} (ha : a.nnr) (hb : b.nnr) : (a * b).sqrt = a.sqrt * b.sqrt

theorem Complex.sqrt_sq_of_nnr {a : ℂ} (h : a.nnr) : (a ^ 2).sqrt = a

@[simp]

theorem Complex.sqrt_sq_nat {n : ℕ} : (OfNat.ofNat n ^ 2).sqrt = OfNat.ofNat n

@[simp]

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