Theorems · Theorem · complex analysis

Complex.hasSum_arctan_aux

∀ {z : ℂ},
  ‖z‖ < 1 →
    Complex.log (1 + z * Complex.I) + -Complex.log (1 - z * Complex.I) =
      Complex.log ((1 + z * Complex.I) / (1 - z * Complex.I))

We can combine the logs in log (1 + z * I) + -log (1 - z * I) into one. This is only used in hasSum_arctan.

Defined in

Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Cited by

1 results in Mathlib

Foundations

Depth 203 from the axioms · uses propext, Classical.choice, Quot.sound