Proposal: Adding a Complex Square Root File to Mathlib4

Stream: mathlib4

[Ilvan]

Hi all,

I’ve written a Lean file implementing a definition of the complex square root (csqrt : ℂ → ℂ) via the principal branch of the logarithm, along with a collection of related theorems (e.g., csqrt x ^ 2 = x, the behavior on the arg, re/im part formulas, etc.). The implementation is noncomputable and consistent with the usual principal square root used in complex analysis.

Would this be of interest to contribute to Mathlib4, or as a basis for enhancing existing complex analysis utilities?

If so, could you please clarify the project policy for : Naming convention/Proof style/Documentation.

[Eric Wieser]

Just to check, under what conditions is csqrt z = z ^ (0.5 : ℂ)? Do they agree globally?

[Ilvan]

(deleted)

[Ilvan]

@Eric Wieser I have

noncomputable def csqrt (x : ℂ) : ℂ :=
  if x = 0 then 0 else Complex.exp ((Complex.log x) * (1 / 2 : ℂ))

So I will check and write theorem but i think forall x

[Ilvan]

For more context : I have already proof

theorem sqrt_sq_iff {a b : ℂ} : a^2 = b ↔ (a = csqrt b ∨ a = - csqrt b)
theorem csqrt_sq_eq_or_neg (x : ℂ) : (csqrt (x^2) = x) ∨ (csqrt (x^2) = -x)
theorem csqrt_sq_eq (x : ℂ) : (csqrt x)^2 = x
theorem csqrt_re (x : ℂ) : (csqrt x).re = Real.sqrt (‖x‖) * Real.cos (x.arg * (1 / 2))
theorem csqrt_im (x : ℂ) : (csqrt x).im = Real.sqrt (‖x‖) * Real.sin (x.arg * (1 / 2))
theorem csqrt_mod (x : ℂ) : norm (csqrt x) = √(norm x)
theorem csqrt_arg (x : ℂ) : arg (csqrt x) = (arg x) / 2

[Ilvan]

So yes @Eric Wieser csqrq_to_pow (x : ℂ) : csqrt x = x ^ (1 / 2 : ℂ) i have wrote a proof

[Eric Wieser]

In that case it's not clear to me how useful adding the definition would be

[Ilvan]

Ok thank you